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 =
Show proof