(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/ty3/pr3.ma".
+include "Basic-1/ty3/pr3.ma".
theorem ty3_cred_pr2:
\forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr2 c v1
c0 (Bind b) t2) c0 t2 (clear_bind b c0 t2) (CHead d (Bind Abbr) u) i H0)
(CHead c0 (Bind b) t) (csubst0_snd_bind b i u t2 t H2 c0)))))))))))))))) c v1
v2 H))))).
+(* COMMENTS
+Initial nodes: 383
+END *)
theorem ty3_cred_pr3:
\forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr3 c v1
(ty3 g (CHead c (Bind b) t3) t4 t5))))))).(\lambda (b: B).(\lambda (t0:
T).(\lambda (t4: T).(\lambda (H3: (ty3 g (CHead c (Bind b) t1) t0 t4)).(H2 b
t0 t4 (ty3_cred_pr2 g c t1 t2 H0 b t0 t4 H3)))))))))))) v1 v2 H))))).
+(* COMMENTS
+Initial nodes: 215
+END *)
theorem ty3_gen_lift:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h:
x2 x5 H21 x3 x4 H18 (pc3_gen_lift c0 x4 x2 h x1 H17 e H6)) x5 H21)))))
H19))))) H16)))) t3 H8))))) x0 H7)))))) (lift_gen_flat Cast t3 t2 x0 h x1
H5))))))))))))))) c y x H0))))) H))))))).
+(* COMMENTS
+Initial nodes: 9781
+END *)
theorem ty3_tred:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
(\lambda (t: T).(ty3 g c t1 t)) (ty3 g c u t2) (\lambda (x: T).(\lambda (H1:
(ty3 g c t1 x)).(let H_y \def (ty3_sred_pr3 c t1 t2 H0 g x H1) in (ty3_conv g
c t2 x H_y u t1 H (pc3_pr3_r c t1 t2 H0))))) (ty3_correct g c u t1 H)))))))).
+(* COMMENTS
+Initial nodes: 121
+END *)
theorem ty3_sconv_pc3:
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(let H_y \def
(ty3_sred_pr3 c u2 x H4 g t2 H0) in (let H_y0 \def (ty3_sred_pr3 c u1 x H3 g
t1 H) in (ty3_unique g c x t1 H_y0 t2 H_y)))))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
theorem ty3_sred_back:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t0: T).((ty3 g c
t3)) (ty3 g c t1 t) (\lambda (x: T).(\lambda (H2: (ty3 g c t x)).(ty3_conv g
c t x H2 t1 t0 H (ty3_unique g c t2 t0 (ty3_sred_pr3 c t1 t2 H0 g t0 H) t
H1)))) (ty3_correct g c t2 t H1)))))))))).
+(* COMMENTS
+Initial nodes: 137
+END *)
theorem ty3_sconv:
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
(t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t)) (ty3 g c u1 t2) (\lambda
(x: T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(ty3_sred_back
g c u1 t1 H x H3 t2 (ty3_sred_pr3 c u2 x H4 g t2 H0))))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 129
+END *)