DEFINITION f_equal()
TYPE =
       ∀A:Set.∀B:Set.∀f:A→B.∀x:A.∀y:A.(eq A x y)→(eq B (f x) (f y))
BODY =
        assume A: Set
        assume B: Set
        assume f: A→B
        assume x: A
        assume y: A
        suppose H: eq A x y
          we proceed by induction on H to prove eq B (f x) (f y)
             case refl_equal : ⇒
                the thesis becomes eq B (f x) (f x)
                   by (refl_equal . .)
eq B (f x) (f x)
          we proved eq B (f x) (f y)
       we proved ∀A:Set.∀B:Set.∀f:A→B.∀x:A.∀y:A.(eq A x y)→(eq B (f x) (f y))