-include "Legacy-1/coq/defs.ma".
-
-theorem f_equal:
- \forall (A: Set).(\forall (B: Set).(\forall (f: ((A \to B))).(\forall (x:
-A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
-\def
- \lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x:
-A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B
-(f x) (f a))) (refl_equal B (f x)) y H)))))).
-(* COMMENTS
-Initial nodes: 51
-END *)
-
-theorem f_equal2:
- \forall (A1: Set).(\forall (A2: Set).(\forall (B: Set).(\forall (f: ((A1 \to
-(A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2: A2).(\forall
-(y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2) (f y1
-y2)))))))))))
-\def
- \lambda (A1: Set).(\lambda (A2: Set).(\lambda (B: Set).(\lambda (f: ((A1 \to
-(A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda
-(y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2
-x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind
-A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2
-H0)) y1 H))))))))).
-(* COMMENTS
-Initial nodes: 109
-END *)
-
-theorem f_equal3:
- \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 *)
-
-theorem sym_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
+include "legacy_1/coq/fwd.ma".
+
+lemma f_equal:
+ \forall (A: Type[0]).(\forall (B: Type[0]).(\forall (f: ((A \to
+B))).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
+\def
+ \lambda (A: Type[0]).(\lambda (B: Type[0]).(\lambda (f: ((A \to
+B))).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x
+(\lambda (a: A).(eq B (f x) (f a))) (refl_equal B (f x)) y H)))))).
+
+lemma f_equal2:
+ \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (B: Type[0]).(\forall
+(f: ((A1 \to (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2:
+A2).(\forall (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2)
+(f y1 y2)))))))))))
+\def
+ \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (B: Type[0]).(\lambda
+(f: ((A1 \to (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2:
+A2).(\lambda (y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a:
+A1).((eq A2 x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2
+y2)).(eq_ind A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B
+(f x1 x2)) y2 H0)) y1 H))))))))).
+
+lemma f_equal3:
+ \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)))))))))))).
+
+lemma sym_eq:
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y