(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd".
+include "LambdaDelta-1/ty3/defs.ma".
-include "ty3/defs.ma".
-
-include "pc3/props.ma".
+include "LambdaDelta-1/pc3/props.ma".
theorem ty3_gen_sort:
\forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
(\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)))))).
+theorem tys3_gen_nil:
+ \forall (g: G).(\forall (c: C).(\forall (u: T).((tys3 g c TNil u) \to (ex T
+(\lambda (u0: T).(ty3 g c u u0))))))
+\def
+ \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (H: (tys3 g c TNil
+u)).(insert_eq TList TNil (\lambda (t: TList).(tys3 g c t u)) (\lambda (_:
+TList).(ex T (\lambda (u0: T).(ty3 g c u u0)))) (\lambda (y: TList).(\lambda
+(H0: (tys3 g c y u)).(tys3_ind g c (\lambda (t: TList).(\lambda (t0: T).((eq
+TList t TNil) \to (ex T (\lambda (u0: T).(ty3 g c t0 u0)))))) (\lambda (u0:
+T).(\lambda (u1: T).(\lambda (H1: (ty3 g c u0 u1)).(\lambda (_: (eq TList
+TNil TNil)).(ex_intro T (\lambda (u2: T).(ty3 g c u0 u2)) u1 H1))))) (\lambda
+(t: T).(\lambda (u0: T).(\lambda (_: (ty3 g c t u0)).(\lambda (ts:
+TList).(\lambda (_: (tys3 g c ts u0)).(\lambda (_: (((eq TList ts TNil) \to
+(ex T (\lambda (u1: T).(ty3 g c u0 u1)))))).(\lambda (H4: (eq TList (TCons t
+ts) TNil)).(let H5 \def (eq_ind TList (TCons t ts) (\lambda (ee:
+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)))).
+
+theorem tys3_gen_cons:
+ \forall (g: G).(\forall (c: C).(\forall (ts: TList).(\forall (t: T).(\forall
+(u: T).((tys3 g c (TCons t ts) u) \to (land (ty3 g c t u) (tys3 g c ts
+u)))))))
+\def
+ \lambda (g: G).(\lambda (c: C).(\lambda (ts: TList).(\lambda (t: T).(\lambda
+(u: T).(\lambda (H: (tys3 g c (TCons t ts) u)).(insert_eq TList (TCons t ts)
+(\lambda (t0: TList).(tys3 g c t0 u)) (\lambda (_: TList).(land (ty3 g c t u)
+(tys3 g c ts u))) (\lambda (y: TList).(\lambda (H0: (tys3 g c y u)).(tys3_ind
+g c (\lambda (t0: TList).(\lambda (t1: T).((eq TList t0 (TCons t ts)) \to
+(land (ty3 g c t t1) (tys3 g c ts t1))))) (\lambda (u0: T).(\lambda (u1:
+T).(\lambda (_: (ty3 g c u0 u1)).(\lambda (H2: (eq TList TNil (TCons t
+ts))).(let H3 \def (eq_ind TList TNil (\lambda (ee: TList).(match ee in TList
+return (\lambda (_: TList).Prop) with [TNil \Rightarrow True | (TCons _ _)
+\Rightarrow False])) I (TCons t ts) H2) in (False_ind (land (ty3 g c t u0)
+(tys3 g c ts u0)) H3)))))) (\lambda (t0: T).(\lambda (u0: T).(\lambda (H1:
+(ty3 g c t0 u0)).(\lambda (ts0: TList).(\lambda (H2: (tys3 g c ts0
+u0)).(\lambda (H3: (((eq TList ts0 (TCons t ts)) \to (land (ty3 g c t u0)
+(tys3 g c ts u0))))).(\lambda (H4: (eq TList (TCons t0 ts0) (TCons t
+ts))).(let H5 \def (f_equal TList T (\lambda (e: TList).(match e in TList
+return (\lambda (_: TList).T) with [TNil \Rightarrow t0 | (TCons t1 _)
+\Rightarrow t1])) (TCons t0 ts0) (TCons t ts) H4) in ((let H6 \def (f_equal
+TList TList (\lambda (e: TList).(match e in TList return (\lambda (_:
+TList).TList) with [TNil \Rightarrow ts0 | (TCons _ t1) \Rightarrow t1]))
+(TCons t0 ts0) (TCons t ts) H4) in (\lambda (H7: (eq T t0 t)).(let H8 \def
+(eq_ind TList ts0 (\lambda (t1: TList).((eq TList t1 (TCons t ts)) \to (land
+(ty3 g c t u0) (tys3 g c ts u0)))) H3 ts H6) in (let H9 \def (eq_ind TList
+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)))))).
+