-(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:
+(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: