-H2 \def (eq_ind T (THead (Bind b) v t) (\lambda (ee: T).(match ee in T return
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef x) H1) in
-(False_ind P H2)))) H0))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda
-(_: (((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall
-(P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1
-(TLRef i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H_x \def
-(iso_gen_head (Flat f) t0 (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)
-H0) in (let H1 \def H_x in (ex_2_ind T T (\lambda (v2: T).(\lambda (t2:
-T).(eq T (THead (Bind b) v t) (THead (Flat f) v2 t2)))) P (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f)
-x0 x1))).(let H3 \def (eq_ind T (THead (Bind b) v t) (\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 True | (Flat _) \Rightarrow
-False])])) I (THead (Flat f) x0 x1) H2) in (False_ind P H3))))) H1))))))))
-vs)))))).
-(* COMMENTS
-Initial nodes: 391
-END *)
+H2 \def (eq_ind T (THead (Bind b) v t) (\lambda (ee: T).(match ee with
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
+\Rightarrow True])) I (TLRef x) H1) in (False_ind P H2)))) H0))))) (\lambda
+(t0: T).(\lambda (t1: TList).(\lambda (_: (((iso (THeads (Flat f) t1 (TLRef
+i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P)))).(\lambda (H0: (iso
+(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) (THead (Bind b) v
+t))).(\lambda (P: Prop).(let H_x \def (iso_gen_head (Flat f) t0 (THeads (Flat
+f) t1 (TLRef i)) (THead (Bind b) v t) H0) in (let H1 \def H_x in (ex_2_ind T
+T (\lambda (v2: T).(\lambda (t2: T).(eq T (THead (Bind b) v t) (THead (Flat
+f) v2 t2)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T (THead
+(Bind b) v t) (THead (Flat f) x0 x1))).(let H3 \def (eq_ind T (THead (Bind b)
+v t) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
+\Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat f) x0 x1)
+H2) in (False_ind P H3))))) H1)))))))) vs)))))).