(H18 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H4 u u (pr0_refl u) (Bind b))
(lift (S O) O t4) (pr0_lift t5 t4 H17 (S O) O)))))))) t6 (sym_eq T t6 t4
H15))) t2 H14)) u0 (sym_eq T u0 u H13))) b0 (sym_eq B b0 b H12))) H11)) H10))
-H9 H6 H7))) | (pr0_epsilon t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T
-(THead (Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6
-t4)).((let H9 \def (eq_ind T (THead (Flat Cast) u0 t5) (\lambda (e: T).(match
-e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
+H9 H6 H7))) | (pr0_tau t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T (THead
+(Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6 t4)).((let
+H9 \def (eq_ind T (THead (Flat Cast) u0 t5) (\lambda (e: T).(match e in T
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
+(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
True])])) I (THead (Bind b) u t2) H7) in (False_ind ((eq T t6 t4) \to ((pr0
t5 t6) \to (ty3 g c2 t4 (THead (Bind b) u t3)))) H9)) H8 H6)))]) in (H6
(refl_equal T (THead (Bind b) u t2)) (refl_equal T t4)))))))))))))))))
(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
False])])) I (THead (Flat Appl) w v) H8) in (False_ind ((eq T t4 t2) \to
((not (eq B b Abst)) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w
-(THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) | (pr0_epsilon t3 t4 H6 u0)
+(THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) | (pr0_tau t3 t4 H6 u0)
\Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl)
w v))).(\lambda (H8: (eq T t4 t2)).((let H9 \def (eq_ind T (THead (Flat Cast)
u0 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat
Cast) t3 t2) H8) in (False_ind ((eq T t6 t4) \to ((not (eq B b Abst)) \to
((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))) H10)) H9 H6 H7)))
-| (pr0_epsilon t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast)
-u t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 \def
+| (pr0_tau t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) u
+t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 \def
(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
[(TSort _) \Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7)
\Rightarrow t7])) (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2) H7) in
t0 x)).(ty3_conv g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
(ty3_cast g c2 t3 t0 (H3 c2 H4 t3 (pr0_refl t3)) x H14) t4 t3 (H1 c2 H4 t4
H13) (pc3_pr2_x c2 t3 (THead (Flat Cast) t0 t3) (pr2_free c2 (THead (Flat
-Cast) t0 t3) t3 (pr0_epsilon t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2
-t3 t0 (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))))).
+Cast) t0 t3) t3 (pr0_tau t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2 t3 t0
+(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))))).
theorem ty3_sred_pr0:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (g: G).(\forall