-(vs: TList).(let TMP_4 \def (\lambda (t: TList).((nfs2 c t) \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 (nf2 c TMP_3)))))) in (let TMP_5 \def (\lambda (_: True).H)
-in (let TMP_295 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0:
-(((nfs2 c t0) \to (nf2 c (THeads (Flat Appl) t0 (TLRef i)))))).(\lambda (H1:
-(land (nf2 c t) (nfs2 c t0))).(let H2 \def H1 in (let TMP_6 \def (nf2 c t) in
-(let TMP_7 \def (nfs2 c t0) in (let TMP_8 \def (Flat Appl) in (let TMP_9 \def
-(Flat Appl) in (let TMP_10 \def (TLRef i) in (let TMP_11 \def (THeads TMP_9
-t0 TMP_10) in (let TMP_12 \def (THead TMP_8 t TMP_11) in (let TMP_13 \def
-(nf2 c TMP_12) in (let TMP_294 \def (\lambda (H3: (nf2 c t)).(\lambda (H4:
-(nfs2 c t0)).(let H_y \def (H0 H4) in (\lambda (t2: T).(\lambda (H5: (pr2 c
-(THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2)).(let TMP_14 \def
-(Flat Appl) in (let TMP_15 \def (TLRef i) in (let TMP_16 \def (THeads TMP_14
-t0 TMP_15) in (let H6 \def (pr2_gen_appl c t TMP_16 t2 H5) in (let TMP_19
-\def (\lambda (u2: T).(\lambda (t3: T).(let TMP_17 \def (Flat Appl) in (let
-TMP_18 \def (THead TMP_17 u2 t3) in (eq T t2 TMP_18))))) in (let TMP_20 \def
-(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))) in (let TMP_24 \def (\lambda
-(_: T).(\lambda (t3: T).(let TMP_21 \def (Flat Appl) in (let TMP_22 \def
-(TLRef i) in (let TMP_23 \def (THeads TMP_21 t0 TMP_22) in (pr2 c TMP_23
-t3)))))) in (let TMP_25 \def (ex3_2 T T TMP_19 TMP_20 TMP_24) in (let TMP_31
-\def (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(let
-TMP_26 \def (Flat Appl) in (let TMP_27 \def (TLRef i) in (let TMP_28 \def
-(THeads TMP_26 t0 TMP_27) in (let TMP_29 \def (Bind Abst) in (let TMP_30 \def
-(THead TMP_29 y1 z1) in (eq T TMP_28 TMP_30)))))))))) in (let TMP_34 \def
-(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(let TMP_32
-\def (Bind Abbr) in (let TMP_33 \def (THead TMP_32 u2 t3) in (eq T t2
-TMP_33))))))) in (let TMP_35 \def (\lambda (_: T).(\lambda (_: T).(\lambda
-(u2: T).(\lambda (_: T).(pr2 c t u2))))) in (let TMP_38 \def (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
-(u: T).(let TMP_36 \def (Bind b) in (let TMP_37 \def (CHead c TMP_36 u) in
-(pr2 TMP_37 z1 t3))))))))) in (let TMP_39 \def (ex4_4 T T T T TMP_31 TMP_34
-TMP_35 TMP_38) in (let TMP_41 \def (\lambda (b: B).(\lambda (_: T).(\lambda
-(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(let TMP_40 \def (eq B
-b Abst) in (not TMP_40)))))))) in (let TMP_47 \def (\lambda (b: B).(\lambda
-(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(let
-TMP_42 \def (Flat Appl) in (let TMP_43 \def (TLRef i) in (let TMP_44 \def
-(THeads TMP_42 t0 TMP_43) in (let TMP_45 \def (Bind b) in (let TMP_46 \def
-(THead TMP_45 y1 z1) in (eq T TMP_44 TMP_46)))))))))))) in (let TMP_54 \def
-(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda
-(u2: T).(\lambda (y2: T).(let TMP_48 \def (Bind b) in (let TMP_49 \def (Flat
-Appl) in (let TMP_50 \def (S O) in (let TMP_51 \def (lift TMP_50 O u2) in
-(let TMP_52 \def (THead TMP_49 TMP_51 z2) in (let TMP_53 \def (THead TMP_48
-y2 TMP_52) in (eq T t2 TMP_53))))))))))))) in (let TMP_55 \def (\lambda (_:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
-(_: T).(pr2 c t u2))))))) in (let TMP_56 \def (\lambda (_: B).(\lambda (y1:
-T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
-y2))))))) in (let TMP_59 \def (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
-T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(let TMP_57 \def (Bind
-b) in (let TMP_58 \def (CHead c TMP_57 y2) in (pr2 TMP_58 z1 z2))))))))) in
-(let TMP_60 \def (ex6_6 B T T T T T TMP_41 TMP_47 TMP_54 TMP_55 TMP_56
-TMP_59) in (let TMP_61 \def (Flat Appl) in (let TMP_62 \def (Flat Appl) in
-(let TMP_63 \def (TLRef i) in (let TMP_64 \def (THeads TMP_62 t0 TMP_63) in
-(let TMP_65 \def (THead TMP_61 t TMP_64) in (let TMP_66 \def (eq T TMP_65 t2)
-in (let TMP_132 \def (\lambda (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
-T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_:
-T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (THeads (Flat Appl)
-t0 (TLRef i)) t3))))).(let TMP_69 \def (\lambda (u2: T).(\lambda (t3: T).(let
-TMP_67 \def (Flat Appl) in (let TMP_68 \def (THead TMP_67 u2 t3) in (eq T t2
-TMP_68))))) in (let TMP_70 \def (\lambda (u2: T).(\lambda (_: T).(pr2 c t
-u2))) in (let TMP_74 \def (\lambda (_: T).(\lambda (t3: T).(let TMP_71 \def
-(Flat Appl) in (let TMP_72 \def (TLRef i) in (let TMP_73 \def (THeads TMP_71
-t0 TMP_72) in (pr2 c TMP_73 t3)))))) in (let TMP_75 \def (Flat Appl) in (let
-TMP_76 \def (Flat Appl) in (let TMP_77 \def (TLRef i) in (let TMP_78 \def
-(THeads TMP_76 t0 TMP_77) in (let TMP_79 \def (THead TMP_75 t TMP_78) in (let
-TMP_80 \def (eq T TMP_79 t2) in (let TMP_131 \def (\lambda (x0: T).(\lambda
-(x1: T).(\lambda (H8: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H9: (pr2
-c t x0)).(\lambda (H10: (pr2 c (THeads (Flat Appl) t0 (TLRef i)) x1)).(let
-TMP_81 \def (Flat Appl) in (let TMP_82 \def (THead TMP_81 x0 x1) in (let
-TMP_88 \def (\lambda (t1: T).(let TMP_83 \def (Flat Appl) in (let TMP_84 \def
-(Flat Appl) in (let TMP_85 \def (TLRef i) in (let TMP_86 \def (THeads TMP_84
-t0 TMP_85) in (let TMP_87 \def (THead TMP_83 t TMP_86) in (eq T TMP_87
-t1))))))) in (let TMP_92 \def (\lambda (t1: T).(let TMP_89 \def (Flat Appl)
-in (let TMP_90 \def (TLRef i) in (let TMP_91 \def (THeads TMP_89 t0 TMP_90)
-in (pr2 c TMP_91 t1))))) in (let TMP_93 \def (Flat Appl) in (let TMP_94 \def
-(TLRef i) in (let TMP_95 \def (THeads TMP_93 t0 TMP_94) in (let TMP_96 \def
-(H_y x1 H10) in (let H11 \def (eq_ind_r T x1 TMP_92 H10 TMP_95 TMP_96) in
-(let TMP_97 \def (Flat Appl) in (let TMP_98 \def (TLRef i) in (let TMP_99
-\def (THeads TMP_97 t0 TMP_98) in (let TMP_107 \def (\lambda (t1: T).(let
-TMP_100 \def (Flat Appl) in (let TMP_101 \def (Flat Appl) in (let TMP_102
-\def (TLRef i) in (let TMP_103 \def (THeads TMP_101 t0 TMP_102) in (let
-TMP_104 \def (THead TMP_100 t TMP_103) in (let TMP_105 \def (Flat Appl) in
-(let TMP_106 \def (THead TMP_105 x0 t1) in (eq T TMP_104 TMP_106))))))))) in
-(let TMP_108 \def (\lambda (t1: T).(pr2 c t t1)) in (let TMP_109 \def (H3 x0
-H9) in (let H12 \def (eq_ind_r T x0 TMP_108 H9 t TMP_109) in (let TMP_120
-\def (\lambda (t1: T).(let TMP_110 \def (Flat Appl) in (let TMP_111 \def
-(Flat Appl) in (let TMP_112 \def (TLRef i) in (let TMP_113 \def (THeads
-TMP_111 t0 TMP_112) in (let TMP_114 \def (THead TMP_110 t TMP_113) in (let
-TMP_115 \def (Flat Appl) in (let TMP_116 \def (Flat Appl) in (let TMP_117
-\def (TLRef i) in (let TMP_118 \def (THeads TMP_116 t0 TMP_117) in (let
-TMP_119 \def (THead TMP_115 t1 TMP_118) in (eq T TMP_114 TMP_119))))))))))))
-in (let TMP_121 \def (Flat Appl) in (let TMP_122 \def (Flat Appl) in (let
-TMP_123 \def (TLRef i) in (let TMP_124 \def (THeads TMP_122 t0 TMP_123) in
-(let TMP_125 \def (THead TMP_121 t TMP_124) in (let TMP_126 \def (refl_equal
-T TMP_125) in (let TMP_127 \def (H3 x0 H9) in (let TMP_128 \def (eq_ind T t
-TMP_120 TMP_126 x0 TMP_127) in (let TMP_129 \def (H_y x1 H10) in (let TMP_130
-\def (eq_ind T TMP_99 TMP_107 TMP_128 x1 TMP_129) in (eq_ind_r T TMP_82
-TMP_88 TMP_130 t2 H8))))))))))))))))))))))))))))))))) in (ex3_2_ind T T
-TMP_69 TMP_70 TMP_74 TMP_80 TMP_131 H7)))))))))))) in (let TMP_201 \def
-(\lambda (H7: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
-T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst)
-y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
-T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
-T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))))) (\lambda (_: T).(\lambda
-(z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2
-(CHead c (Bind b) u) z1 t3))))))))).(let TMP_138 \def (\lambda (y1:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(let TMP_133 \def (Flat
-Appl) in (let TMP_134 \def (TLRef i) in (let TMP_135 \def (THeads TMP_133 t0
-TMP_134) in (let TMP_136 \def (Bind Abst) in (let TMP_137 \def (THead TMP_136
-y1 z1) in (eq T TMP_135 TMP_137)))))))))) in (let TMP_141 \def (\lambda (_:
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(let TMP_139 \def (Bind
-Abbr) in (let TMP_140 \def (THead TMP_139 u2 t3) in (eq T t2 TMP_140)))))))
-in (let TMP_142 \def (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
-T).(\lambda (_: T).(pr2 c t u2))))) in (let TMP_145 \def (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
-(u: T).(let TMP_143 \def (Bind b) in (let TMP_144 \def (CHead c TMP_143 u) in
-(pr2 TMP_144 z1 t3))))))))) in (let TMP_146 \def (Flat Appl) in (let TMP_147
-\def (Flat Appl) in (let TMP_148 \def (TLRef i) in (let TMP_149 \def (THeads
-TMP_147 t0 TMP_148) in (let TMP_150 \def (THead TMP_146 t TMP_149) in (let
-TMP_151 \def (eq T TMP_150 t2) in (let TMP_200 \def (\lambda (x0: T).(\lambda
-(x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T (THeads (Flat
-Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1))).(\lambda (H9: (eq T t2 (THead
-(Bind Abbr) x2 x3))).(\lambda (_: (pr2 c t x2)).(\lambda (_: ((\forall (b:
-B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let TMP_152 \def
-(Bind Abbr) in (let TMP_153 \def (THead TMP_152 x2 x3) in (let TMP_159 \def
-(\lambda (t1: T).(let TMP_154 \def (Flat Appl) in (let TMP_155 \def (Flat
-Appl) in (let TMP_156 \def (TLRef i) in (let TMP_157 \def (THeads TMP_155 t0
-TMP_156) in (let TMP_158 \def (THead TMP_154 t TMP_157) in (eq T TMP_158
-t1))))))) in (let TMP_167 \def (\lambda (t1: TList).((nf2 c (THeads (Flat
-Appl) t1 (TLRef i))) \to ((eq T (THeads (Flat Appl) t1 (TLRef i)) (THead
-(Bind Abst) x0 x1)) \to (let TMP_160 \def (Flat Appl) in (let TMP_161 \def
-(Flat Appl) in (let TMP_162 \def (TLRef i) in (let TMP_163 \def (THeads
-TMP_161 t1 TMP_162) in (let TMP_164 \def (THead TMP_160 t TMP_163) in (let
-TMP_165 \def (Bind Abbr) in (let TMP_166 \def (THead TMP_165 x2 x3) in (eq T
-TMP_164 TMP_166))))))))))) in (let TMP_180 \def (\lambda (_: (nf2 c (THeads
-(Flat Appl) TNil (TLRef i)))).(\lambda (H13: (eq T (THeads (Flat Appl) TNil
-(TLRef i)) (THead (Bind Abst) x0 x1))).(let TMP_168 \def (TLRef i) in (let
-TMP_169 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) in (let
-TMP_170 \def (Bind Abst) in (let TMP_171 \def (THead TMP_170 x0 x1) in (let
-H14 \def (eq_ind T TMP_168 TMP_169 I TMP_171 H13) in (let TMP_172 \def (Flat
-Appl) in (let TMP_173 \def (Flat Appl) in (let TMP_174 \def (TLRef i) in (let
-TMP_175 \def (THeads TMP_173 TNil TMP_174) in (let TMP_176 \def (THead
-TMP_172 t TMP_175) in (let TMP_177 \def (Bind Abbr) in (let TMP_178 \def
-(THead TMP_177 x2 x3) in (let TMP_179 \def (eq T TMP_176 TMP_178) in
-(False_ind TMP_179 H14)))))))))))))))) in (let TMP_198 \def (\lambda (t1:
-T).(\lambda (t3: TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef
-i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind Abst) x0 x1))
-\to (eq T (THead (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead
-(Bind Abbr) x2 x3)))))).(\lambda (_: (nf2 c (THeads (Flat Appl) (TCons t1 t3)
-(TLRef i)))).(\lambda (H13: (eq T (THeads (Flat Appl) (TCons t1 t3) (TLRef
-i)) (THead (Bind Abst) x0 x1))).(let TMP_181 \def (Flat Appl) in (let TMP_182
-\def (Flat Appl) in (let TMP_183 \def (TLRef i) in (let TMP_184 \def (THeads
-TMP_182 t3 TMP_183) in (let TMP_185 \def (THead TMP_181 t1 TMP_184) in (let
-TMP_186 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind
-_) \Rightarrow False | (Flat _) \Rightarrow True])])) in (let TMP_187 \def
-(Bind Abst) in (let TMP_188 \def (THead TMP_187 x0 x1) in (let H14 \def
-(eq_ind T TMP_185 TMP_186 I TMP_188 H13) in (let TMP_189 \def (Flat Appl) in
-(let TMP_190 \def (Flat Appl) in (let TMP_191 \def (TCons t1 t3) in (let
-TMP_192 \def (TLRef i) in (let TMP_193 \def (THeads TMP_190 TMP_191 TMP_192)
-in (let TMP_194 \def (THead TMP_189 t TMP_193) in (let TMP_195 \def (Bind
-Abbr) in (let TMP_196 \def (THead TMP_195 x2 x3) in (let TMP_197 \def (eq T
-TMP_194 TMP_196) in (False_ind TMP_197 H14)))))))))))))))))))))))) in (let
-TMP_199 \def (TList_ind TMP_167 TMP_180 TMP_198 t0 H_y H8) in (eq_ind_r T
-TMP_153 TMP_159 TMP_199 t2 H9)))))))))))))))) in (ex4_4_ind T T T T TMP_138
-TMP_141 TMP_142 TMP_145 TMP_151 TMP_200 H7))))))))))))) in (let TMP_293 \def
-(\lambda (H7: (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: