-(vs: TList).(TList_ind (\lambda (t: TList).(\forall (u: T).((pr3 c (THeads
-(Flat Appl) t (TLRef i)) u) \to (iso (THeads (Flat Appl) t (TLRef i)) u))))
-(\lambda (u: T).(\lambda (H0: (pr3 c (TLRef i) u)).(let H_y \def
-(nf2_pr3_unfold c (TLRef i) u H0 H) in (let H1 \def (eq_ind_r T u (\lambda
-(t: T).(pr3 c (TLRef i) t)) H0 (TLRef i) H_y) in (eq_ind T (TLRef i) (\lambda
-(t: T).(iso (TLRef i) t)) (iso_refl (TLRef i)) u H_y))))) (\lambda (t:
-T).(\lambda (t0: TList).(\lambda (H0: ((\forall (u: T).((pr3 c (THeads (Flat
-Appl) t0 (TLRef i)) u) \to (iso (THeads (Flat Appl) t0 (TLRef i))
-u))))).(\lambda (u: T).(\lambda (H1: (pr3 c (THead (Flat Appl) t (THeads
-(Flat Appl) t0 (TLRef i))) u)).(let H2 \def (pr3_gen_appl c t (THeads (Flat
-Appl) t0 (TLRef i)) u H1) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda
-(t2: T).(eq T u (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
-T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c (THeads (Flat Appl)
-t0 (TLRef i)) t2)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda
-(u2: T).(\lambda (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) u))))) (\lambda (_:
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))) (\lambda
-(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THeads (Flat
-Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
-(z1: T).(\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u0:
-T).(pr3 (CHead c (Bind b) u0) z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b:
+(vs: TList).(let TMP_4 \def (\lambda (t: TList).(\forall (u: T).((pr3 c
+(THeads (Flat Appl) t (TLRef i)) u) \to (let TMP_1 \def (Flat Appl) in (let
+TMP_2 \def (TLRef i) in (let TMP_3 \def (THeads TMP_1 t TMP_2) in (iso TMP_3
+u))))))) in (let TMP_14 \def (\lambda (u: T).(\lambda (H0: (pr3 c (TLRef i)
+u)).(let TMP_5 \def (TLRef i) in (let H_y \def (nf2_pr3_unfold c TMP_5 u H0
+H) in (let TMP_7 \def (\lambda (t: T).(let TMP_6 \def (TLRef i) in (pr3 c
+TMP_6 t))) in (let TMP_8 \def (TLRef i) in (let H1 \def (eq_ind_r T u TMP_7
+H0 TMP_8 H_y) in (let TMP_9 \def (TLRef i) in (let TMP_11 \def (\lambda (t:
+T).(let TMP_10 \def (TLRef i) in (iso TMP_10 t))) in (let TMP_12 \def (TLRef
+i) in (let TMP_13 \def (iso_refl TMP_12) in (eq_ind T TMP_9 TMP_11 TMP_13 u
+H_y)))))))))))) in (let TMP_162 \def (\lambda (t: T).(\lambda (t0:
+TList).(\lambda (H0: ((\forall (u: T).((pr3 c (THeads (Flat Appl) t0 (TLRef
+i)) u) \to (iso (THeads (Flat Appl) t0 (TLRef i)) u))))).(\lambda (u:
+T).(\lambda (H1: (pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef
+i))) u)).(let TMP_15 \def (Flat Appl) in (let TMP_16 \def (TLRef i) in (let
+TMP_17 \def (THeads TMP_15 t0 TMP_16) in (let H2 \def (pr3_gen_appl c t
+TMP_17 u H1) in (let TMP_20 \def (\lambda (u2: T).(\lambda (t2: T).(let
+TMP_18 \def (Flat Appl) in (let TMP_19 \def (THead TMP_18 u2 t2) in (eq T u
+TMP_19))))) in (let TMP_21 \def (\lambda (u2: T).(\lambda (_: T).(pr3 c t
+u2))) in (let TMP_25 \def (\lambda (_: T).(\lambda (t2: T).(let TMP_22 \def
+(Flat Appl) in (let TMP_23 \def (TLRef i) in (let TMP_24 \def (THeads TMP_22
+t0 TMP_23) in (pr3 c TMP_24 t2)))))) in (let TMP_26 \def (ex3_2 T T TMP_20
+TMP_21 TMP_25) in (let TMP_29 \def (\lambda (_: T).(\lambda (_: T).(\lambda
+(u2: T).(\lambda (t2: T).(let TMP_27 \def (Bind Abbr) in (let TMP_28 \def
+(THead TMP_27 u2 t2) in (pr3 c TMP_28 u))))))) in (let TMP_30 \def (\lambda
+(_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))) in
+(let TMP_36 \def (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
+(_: T).(let TMP_31 \def (Flat Appl) in (let TMP_32 \def (TLRef i) in (let
+TMP_33 \def (THeads TMP_31 t0 TMP_32) in (let TMP_34 \def (Bind Abst) in (let
+TMP_35 \def (THead TMP_34 y1 z1) in (pr3 c TMP_33 TMP_35)))))))))) in (let
+TMP_39 \def (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2:
+T).(\forall (b: B).(\forall (u0: T).(let TMP_37 \def (Bind b) in (let TMP_38
+\def (CHead c TMP_37 u0) in (pr3 TMP_38 z1 t2))))))))) in (let TMP_40 \def
+(ex4_4 T T T T TMP_29 TMP_30 TMP_36 TMP_39) in (let TMP_42 \def (\lambda (b: