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