(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/ty3/defs.ma".
+include "Basic-1/ty3/defs.ma".
-include "LambdaDelta-1/pc3/props.ma".
+include "Basic-1/pc3/props.ma".
theorem ty3_gen_sort:
\forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
(TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n)
H5) in (False_ind (pc3 c0 (TSort (next g n)) (THead (Flat Cast) t0 t2))
H6))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 1179
+END *)
theorem ty3_gen_lref:
\forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
(\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
t)))))) H6))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 5569
+END *)
theorem ty3_gen_bind:
\forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1:
(THead (Flat Cast) t3 t2)))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u t)))
(\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4))))
H6))))))))))) c y x H0))) H))))))).
+(* COMMENTS
+Initial nodes: 3389
+END *)
theorem ty3_gen_appl:
\forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x:
(THead (Flat Cast) t0 t2)))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v
(THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u))))
H6))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 3171
+END *)
theorem ty3_gen_cast:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall
Cast) t5 t2) (THead (Flat Cast) t4 t2))) (\lambda (_: T).(ty3 g c0 t1 t2))
(\lambda (t5: T).(ty3 g c0 t2 t5)) t4 (pc3_refl c0 (THead (Flat Cast) t4 t2))
H14 H10))) t3 H8))))))) H6))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2609
+END *)
theorem tys3_gen_nil:
\forall (g: G).(\forall (c: C).(\forall (u: T).((tys3 g c TNil u) \to (ex T
TList).(match ee in TList return (\lambda (_: TList).Prop) with [TNil
\Rightarrow False | (TCons _ _) \Rightarrow True])) I TNil H4) in (False_ind
(ex T (\lambda (u1: T).(ty3 g c u0 u1))) H5))))))))) y u H0))) H)))).
+(* COMMENTS
+Initial nodes: 255
+END *)
theorem tys3_gen_cons:
\forall (g: G).(\forall (c: C).(\forall (ts: TList).(\forall (t: T).(\forall
ts0 (\lambda (t1: TList).(tys3 g c t1 u0)) H2 ts H6) in (let H10 \def (eq_ind
T t0 (\lambda (t1: T).(ty3 g c t1 u0)) H1 t H7) in (conj (ty3 g c t u0) (tys3
g c ts u0) H10 H9)))))) H5))))))))) y u H0))) H)))))).
+(* COMMENTS
+Initial nodes: 479
+END *)