(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2025 --  Inria - CNRS - Paris-Saclay University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)

(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.

Require Import ClassicalEpsilon.

Lemma function_extensionality:
  forall A B (f g : A -> B),
    (forall x, f x = g x) -> f = g.
Admitted.

(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}
    (m1:a -> b) (m2:a -> b) : Prop :=
  forall (x:a), ((m1 x) = (m2 x)).

Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).

(* Why3 goal *)
Lemma extensionality {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
  forall (m1:a -> b) (m2:a -> b), infix_eqeq m1 m2 -> (m1 = m2).
Proof.
intros m1 m2 h1.
apply function_extensionality.
intros x.
generalize (h1 x).
easy.
Qed.