-(THead (Bind b) u t1) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T
-(\lambda (u0: T).(eq T u2 (lift (S i) O u0)))) H9))))))))))))))))) (\lambda
-(c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w u)).(\lambda
-(_: (((eq T w (TLRef i)) \to ((nf2 c0 w) \to (\forall (u2: T).((nf2 c0 u2)
-\to ((pc3 c0 u u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
-u0))))))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead
-(Bind Abst) u t))).(\lambda (_: (((eq T v (TLRef i)) \to ((nf2 c0 v) \to
-(\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 (THead (Bind Abst) u t) u2) \to
-(ex T (\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (H5: (eq
-T (THead (Flat Appl) w v) (TLRef i))).(\lambda (_: (nf2 c0 (THead (Flat Appl)
-w v))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead
-(Flat Appl) w (THead (Bind Abst) u t)) u2)).(let H9 \def (eq_ind T (THead
-(Flat Appl) w v) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
-with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
-_) \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T (\lambda (u0:
-T).(eq T u2 (lift (S i) O u0)))) H9)))))))))))))))) (\lambda (c0: C).(\lambda
-(t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T
-t1 (TLRef i)) \to ((nf2 c0 t1) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0
-t2 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))).(\lambda
-(t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (_: (((eq T t2 (TLRef i)) \to
-((nf2 c0 t2) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 t0 u2) \to (ex T
-(\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))).(\lambda (H5: (eq T
-(THead (Flat Cast) t2 t1) (TLRef i))).(\lambda (_: (nf2 c0 (THead (Flat Cast)
-t2 t1))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0
-(THead (Flat Cast) t0 t2) u2)).(let H9 \def (eq_ind T (THead (Flat Cast) t2
-t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
-_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
-\Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T (\lambda (u: T).(eq T
-u2 (lift (S i) O u)))) H9))))))))))))))) c y u1 H0))) H))))).
-(* COMMENTS
-Initial nodes: 2175
-END *)
+(THead (Bind b) u t1) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow
+False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
+(TLRef i) H5) in (False_ind (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
+u0)))) H9))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u:
+T).(\lambda (_: (ty3 g c0 w u)).(\lambda (_: (((eq T w (TLRef i)) \to ((nf2
+c0 w) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 u u2) \to (ex T (\lambda
+(u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (v: T).(\lambda (t:
+T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (_: (((eq T v
+(TLRef i)) \to ((nf2 c0 v) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0
+(THead (Bind Abst) u t) u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
+u0))))))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (TLRef
+i))).(\lambda (_: (nf2 c0 (THead (Flat Appl) w v))).(\lambda (u2: T).(\lambda
+(_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst)
+u t)) u2)).(let H9 \def (eq_ind T (THead (Flat Appl) w v) (\lambda (ee:
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
+| (THead _ _ _) \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T
+(\lambda (u0: T).(eq T u2 (lift (S i) O u0)))) H9)))))))))))))))) (\lambda
+(c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1
+t2)).(\lambda (_: (((eq T t1 (TLRef i)) \to ((nf2 c0 t1) \to (\forall (u2:
+T).((nf2 c0 u2) \to ((pc3 c0 t2 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift
+(S i) O u))))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda
+(_: (((eq T t2 (TLRef i)) \to ((nf2 c0 t2) \to (\forall (u2: T).((nf2 c0 u2)
+\to ((pc3 c0 t0 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O
+u))))))))))).(\lambda (H5: (eq T (THead (Flat Cast) t2 t1) (TLRef
+i))).(\lambda (_: (nf2 c0 (THead (Flat Cast) t2 t1))).(\lambda (u2:
+T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead (Flat Cast) t0 t2)
+u2)).(let H9 \def (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match
+ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _
+_ _) \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T (\lambda (u:
+T).(eq T u2 (lift (S i) O u)))) H9))))))))))))))) c y u1 H0))) H))))).