DEFINITION f_equal3()
TYPE =
       ∀A1:Set
         .∀A2:Set
           .∀A3:Set
             .∀B:Set
               .∀f:A1→A2→A3→B
                 .∀x1:A1.∀y1:A1.∀x2:A2.∀y2:A2.∀x3:A3.∀y3:A3.(eq A1 x1 y1)→(eq A2 x2 y2)→(eq A3 x3 y3)→(eq B (f x1 x2 x3) (f y1 y2 y3))
BODY =
Show proof