(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))))).
(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))))).
(\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))))).
(\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))))).
(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))))))).
(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))))))).
(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)))))).
(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)))))).
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)))))).
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)))))).
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)))).
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)))).
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)))))).
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)))))).