DEFINITION f_equal2()
TYPE =
       ∀A1:Set
         .∀A2:Set.∀B:Set.∀f:A1→A2→B.∀x1:A1.∀y1:A1.∀x2:A2.∀y2:A2.(eq A1 x1 y1)→(eq A2 x2 y2)→(eq B (f x1 x2) (f y1 y2))
BODY =
        assume A1: Set
        assume A2: Set
        assume B: Set
        assume f: A1→A2→B
        assume x1: A1
        assume y1: A1
        assume x2: A2
        assume y2: A2
        suppose H: eq A1 x1 y1
          we proceed by induction on H to prove (eq A2 x2 y2)→(eq B (f x1 x2) (f y1 y2))
             case refl_equal : ⇒
                the thesis becomes (eq A2 x2 y2)→(eq B (f x1 x2) (f x1 y2))
                   suppose H0: eq A2 x2 y2
                      we proceed by induction on H0 to prove eq B (f x1 x2) (f x1 y2)
                         case refl_equal : ⇒
                            the thesis becomes eq B (f x1 x2) (f x1 x2)
                               by (refl_equal . .)
eq B (f x1 x2) (f x1 x2)
                      we proved eq B (f x1 x2) (f x1 y2)
(eq A2 x2 y2)→(eq B (f x1 x2) (f x1 y2))
          we proved (eq A2 x2 y2)→(eq B (f x1 x2) (f y1 y2))
       we proved 
          ∀A1:Set
            .∀A2:Set.∀B:Set.∀f:A1→A2→B.∀x1:A1.∀y1:A1.∀x2:A2.∀y2:A2.(eq A1 x1 y1)→(eq A2 x2 y2)→(eq B (f x1 x2) (f y1 y2))