(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubt/ty3.ma".
+include "Basic-1/csubt/ty3.ma".
-include "LambdaDelta-1/ty3/subst1.ma".
+include "Basic-1/ty3/subst1.ma".
-include "LambdaDelta-1/ty3/fsubst0.ma".
+include "Basic-1/ty3/fsubst0.ma".
-include "LambdaDelta-1/pc3/pc1.ma".
+include "Basic-1/pc3/pc1.ma".
-include "LambdaDelta-1/pc3/wcpr0.ma".
+include "Basic-1/pc3/wcpr0.ma".
-include "LambdaDelta-1/pc1/props.ma".
+include "Basic-1/pc1/props.ma".
theorem ty3_sred_wcpr0_pr0:
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1
(H3 c2 H4 t3 (pr0_refl t3))))) t6 (sym_eq T t6 t4 H12))) t5 (sym_eq T t5 t2
H11))) u (sym_eq T u t3 H10))) H9)) H8 H6)))]) in (H6 (refl_equal T (THead
(Flat Cast) t3 t2)) (refl_equal T t4))))))))))))))) c1 t1 t H))))).
+(* COMMENTS
+Initial nodes: 14710
+END *)
theorem ty3_sred_pr0:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (g: G).(\forall
\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(\lambda (g:
G).(\lambda (c: C).(\lambda (t: T).(\lambda (H0: (ty3 g c t1
t)).(ty3_sred_wcpr0_pr0 g c t1 t H0 c (wcpr0_refl c) t2 H))))))).
+(* COMMENTS
+Initial nodes: 47
+END *)
theorem ty3_sred_pr1:
\forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall
C).(\forall (t: T).((ty3 g c t3 t) \to (ty3 g c t5 t))))))).(\lambda (g:
G).(\lambda (c: C).(\lambda (t: T).(\lambda (H3: (ty3 g c t4 t)).(H2 g c t
(ty3_sred_pr0 t4 t3 H0 g c t H3)))))))))))) t1 t2 H))).
+(* COMMENTS
+Initial nodes: 151
+END *)
theorem ty3_sred_pr2:
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
G).(\lambda (t0: T).(\lambda (H3: (ty3 g c0 t3 t0)).(ty3_subst0 g c0 t4 t0
(ty3_sred_wcpr0_pr0 g c0 t3 t0 H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t
H2)))))))))))))) c t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 205
+END *)
theorem ty3_sred_pr3:
\forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall
t3 t) \to (ty3 g c t5 t)))))).(\lambda (g: G).(\lambda (t: T).(\lambda (H3:
(ty3 g c t4 t)).(H2 g t (ty3_sred_pr2 c t4 t3 H0 g t H3))))))))))) t1 t2
H)))).
+(* COMMENTS
+Initial nodes: 151
+END *)