-T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
-False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
-(THead (Bind Abst) x3 x5) H22) in (False_ind (ex4_2 T T (\lambda (v:
-T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) TNil
-(TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3
-g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v
-x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x) v))))
-H23))) (\lambda (t2: T).(\lambda (t3: TList).(\lambda (_: (((eq T (THeads
-(Flat Appl) t3 (TLRef x1)) (THead (Bind Abst) x3 x5)) \to (ex4_2 T T (\lambda
-(v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) t3
-(TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3
-g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v
-x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x)
-v))))))).(\lambda (H22: (eq T (THeads (Flat Appl) (TCons t2 t3) (TLRef x1))
-(THead (Bind Abst) x3 x5))).(let H23 \def (eq_ind T (THead (Flat Appl) t2
-(THeads (Flat Appl) t3 (TLRef x1))) (\lambda (ee: T).(match ee 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 Abst) x3 x5) H22) in (False_ind (ex4_2 T T (\lambda
-(v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) (TCons
-t2 t3) (TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0:
-T).(ty3 g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind
-Abst) x) v x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x)
-v)))) H23)))))) t1 H18))))))) H17))))))))) (ty3_gen_appl g c t0 (THeads (Flat
-Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2) H12))))))))) x0)) H10)) H9)) t
-H5))))))) H4)) H3))))))))))).
-(* COMMENTS
-Initial nodes: 5333
-END *)
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
+(THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x3 x5) H22) in
+(False_ind (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Flat
+Appl) t0 (THeads (Flat Appl) TNil (TLRef x1))) (THead (Bind Abst) x v))))
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
+T).(nf2 (CHead c (Bind Abst) x) v)))) H23))) (\lambda (t2: T).(\lambda (t3:
+TList).(\lambda (_: (((eq T (THeads (Flat Appl) t3 (TLRef x1)) (THead (Bind
+Abst) x3 x5)) \to (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead
+(Flat Appl) t0 (THeads (Flat Appl) t3 (TLRef x1))) (THead (Bind Abst) x v))))
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
+T).(nf2 (CHead c (Bind Abst) x) v))))))).(\lambda (H22: (eq T (THeads (Flat
+Appl) (TCons t2 t3) (TLRef x1)) (THead (Bind Abst) x3 x5))).(let H23 \def
+(eq_ind T (THead (Flat Appl) t2 (THeads (Flat Appl) t3 (TLRef x1))) (\lambda
+(ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
+False | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False |
+(Flat _) \Rightarrow True])])) I (THead (Bind Abst) x3 x5) H22) in (False_ind
+(ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0
+(THeads (Flat Appl) (TCons t2 t3) (TLRef x1))) (THead (Bind Abst) x v))))
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
+T).(nf2 (CHead c (Bind Abst) x) v)))) H23)))))) t1 H18))))))) H17)))))))))
+(ty3_gen_appl g c t0 (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x
+x2) H12))))))))) x0)) H10)) H9)) t H5))))))) H4)) H3))))))))))).