- \forall (A1: Set).(\forall (A2: Set).(\forall (A3: Set).(\forall (B:
-Set).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1: A1).(\forall
-(y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3: A3).(\forall (y3:
-A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2
-x3) (f y1 y2 y3)))))))))))))))
-\def
- \lambda (A1: Set).(\lambda (A2: Set).(\lambda (A3: Set).(\lambda (B:
-Set).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1: A1).(\lambda
-(y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3: A3).(\lambda (y3:
-A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2 x2 y2)
-\to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3))))) (\lambda (H0: (eq
-A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3) \to (eq B (f x1 x2
-x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a:
-A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2
-H0)) y1 H)))))))))))).
-(* COMMENTS
-Initial nodes: 183
-END *)
+ \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (A3: Type[0]).(\forall
+(B: Type[0]).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1:
+A1).(\forall (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3:
+A3).(\forall (y3: A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3)
+\to (eq B (f x1 x2 x3) (f y1 y2 y3)))))))))))))))
+\def
+ \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (A3: Type[0]).(\lambda
+(B: Type[0]).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1:
+A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3:
+A3).(\lambda (y3: A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a:
+A1).((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3)))))
+(\lambda (H0: (eq A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3)
+\to (eq B (f x1 x2 x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3
+x3 (\lambda (a: A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2
+x3)) y3 H1)) y2 H0)) y1 H)))))))))))).