-(THead (Bind b) v t)) \to (\forall (P: Prop).P))) in (let TMP_16 \def
-(\lambda (H: (iso (THead (Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P:
-Prop).(let TMP_2 \def (Flat f2) in (let TMP_3 \def (Bind b) in (let TMP_4
-\def (THead TMP_3 v t) in (let H_x \def (iso_gen_head TMP_2 v2 t2 TMP_4 H) in
-(let H0 \def H_x in (let TMP_9 \def (\lambda (v3: T).(\lambda (t3: T).(let
-TMP_5 \def (Bind b) in (let TMP_6 \def (THead TMP_5 v t) in (let TMP_7 \def
-(Flat f2) in (let TMP_8 \def (THead TMP_7 v3 t3) in (eq T TMP_6 TMP_8)))))))
-in (let TMP_15 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T
-(THead (Bind b) v t) (THead (Flat f2) x0 x1))).(let TMP_10 \def (Bind b) in
-(let TMP_11 \def (THead TMP_10 v t) in (let TMP_12 \def (\lambda (ee:
-T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
-| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat
-_) \Rightarrow False])])) in (let TMP_13 \def (Flat f2) in (let TMP_14 \def
-(THead TMP_13 x0 x1) in (let H2 \def (eq_ind T TMP_11 TMP_12 I TMP_14 H1) in
-(False_ind P H2)))))))))) in (ex_2_ind T T TMP_9 P TMP_15 H0)))))))))) in
-(let TMP_35 \def (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_: (((iso
-(THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to
-(\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads (Flat
-f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P:
-Prop).(let TMP_17 \def (Flat f1) in (let TMP_18 \def (Flat f1) in (let TMP_19
-\def (Flat f2) in (let TMP_20 \def (THead TMP_19 v2 t2) in (let TMP_21 \def
-(THeads TMP_18 t1 TMP_20) in (let TMP_22 \def (Bind b) in (let TMP_23 \def
-(THead TMP_22 v t) in (let H_x \def (iso_gen_head TMP_17 t0 TMP_21 TMP_23 H0)
-in (let H1 \def H_x in (let TMP_28 \def (\lambda (v3: T).(\lambda (t3:
-T).(let TMP_24 \def (Bind b) in (let TMP_25 \def (THead TMP_24 v t) in (let
-TMP_26 \def (Flat f1) in (let TMP_27 \def (THead TMP_26 v3 t3) in (eq T
-TMP_25 TMP_27))))))) in (let TMP_34 \def (\lambda (x0: T).(\lambda (x1:
-T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f1) x0 x1))).(let
-TMP_29 \def (Bind b) in (let TMP_30 \def (THead TMP_29 v t) in (let TMP_31
-\def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
-\Rightarrow True | (Flat _) \Rightarrow False])])) in (let TMP_32 \def (Flat
-f1) in (let TMP_33 \def (THead TMP_32 x0 x1) in (let H3 \def (eq_ind T TMP_30
-TMP_31 I TMP_33 H2) in (False_ind P H3)))))))))) in (ex_2_ind T T TMP_28 P
-TMP_34 H1))))))))))))))))) in (TList_ind TMP_1 TMP_16 TMP_35 vs))))))))))).
+(THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead
+(Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H_x \def
+(iso_gen_head (Flat f2) v2 t2 (THead (Bind b) v t) H) in (let H0 \def H_x in
+(ex_2_ind T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b) v t)
+(THead (Flat f2) v3 t3)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1:
+(eq T (THead (Bind b) v t) (THead (Flat f2) x0 x1))).(let H2 \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
+f2) x0 x1) H1) in (False_ind P H2))))) H0))))) (\lambda (t0: T).(\lambda (t1:
+TList).(\lambda (_: (((iso (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))
+(THead (Bind b) v t)) \to (\forall (P: Prop).P)))).(\lambda (H0: (iso (THead
+(Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v
+t))).(\lambda (P: Prop).(let H_x \def (iso_gen_head (Flat f1) t0 (THeads
+(Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t) H0) in (let H1
+\def H_x in (ex_2_ind T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead
+(Bind b) v t) (THead (Flat f1) v3 t3)))) P (\lambda (x0: T).(\lambda (x1:
+T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f1) 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 f1) x0 x1) H2) in (False_ind P H3))))) H1))))))))
+vs)))))))).