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 =
        assume A1: Set
        assume A2: Set
        assume A3: Set
        assume B: Set
        assume f: A1→A2→A3→B
        assume x1: A1
        assume y1: A1
        assume x2: A2
        assume y2: A2
        assume x3: A3
        assume y3: A3
        suppose H: eq A1 x1 y1
          we proceed by induction on H to prove (eq A2 x2 y2)→(eq A3 x3 y3)→(eq B (f x1 x2 x3) (f y1 y2 y3))
             case refl_equal : ⇒
                the thesis becomes (eq A2 x2 y2)→(eq A3 x3 y3)→(eq B (f x1 x2 x3) (f x1 y2 y3))
                   suppose H0: eq A2 x2 y2
                      we proceed by induction on H0 to prove (eq A3 x3 y3)→(eq B (f x1 x2 x3) (f x1 y2 y3))
                         case refl_equal : ⇒
                            the thesis becomes (eq A3 x3 y3)→(eq B (f x1 x2 x3) (f x1 x2 y3))
                               suppose H1: eq A3 x3 y3
                                  we proceed by induction on H1 to prove eq B (f x1 x2 x3) (f x1 x2 y3)
                                     case refl_equal : ⇒
                                        the thesis becomes eq B (f x1 x2 x3) (f x1 x2 x3)
                                           by (refl_equal . .)
eq B (f x1 x2 x3) (f x1 x2 x3)
                                  we proved eq B (f x1 x2 x3) (f x1 x2 y3)
(eq A3 x3 y3)→(eq B (f x1 x2 x3) (f x1 x2 y3))
                      we proved (eq A3 x3 y3)→(eq B (f x1 x2 x3) (f x1 y2 y3))
(eq A2 x2 y2)→(eq A3 x3 y3)→(eq B (f x1 x2 x3) (f x1 y2 y3))
          we proved (eq A2 x2 y2)→(eq A3 x3 y3)→(eq B (f x1 x2 x3) (f y1 y2 y3))
       we proved 
          ∀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))