2
Set Implicit Arguments.
5
Definition feq (f g: A -> B):=forall a, (f a)=(g a).
6
Infix "=f":= feq (at level 80, right associativity).
9
Lemma feq_refl: forall f, f =f f.
13
Lemma feq_sym: forall f g, f =f g-> g =f f.
17
Lemma feq_trans: forall f g h, f =f g-> g =f h -> f =f h.
18
unfold feq. intuition.
23
Infix "=f":= feq (at level 80, right associativity).
24
Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans.
26
Variable K:(nat -> nat)->Prop.
27
Variable K_ext:forall a b, (K a)->(a =f b)->(K b).
29
Add Parametric Relation (A B : Type) : (A -> B) (@feq A B)
30
reflexivity proved by (@feq_refl A B)
31
symmetry proved by (@feq_sym A B)
32
transitivity proved by (@feq_trans A B) as funsetoid.
34
Add Morphism K with signature (@feq nat nat) ==> iff as K_ext1.
35
intuition. apply (K_ext H0 H).
36
intuition. assert (y =f x);auto. apply (K_ext H0 H1).
39
Lemma three:forall n, forall a, (K a)->(a =f (fun m => (a (n+m))))-> (K (fun m