-(asucc g a1) c w) \to (sc3 g a0 c (THeads (Flat Appl) vs (THead (Flat Appl) v
-(THead (Bind Abst) w t)))))))))))))).(\lambda (vs: TList).(\lambda (c:
-C).(\lambda (v: T).(\lambda (t: T).(\lambda (H1: (land (arity g c (THeads
-(Flat Appl) vs (THead (Bind Abbr) v t)) (AHead a a0)) (\forall (d:
-C).(\forall (w: T).((sc3 g a d w) \to (\forall (is: PList).((drop1 is d c)
-\to (sc3 g a0 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs (THead
-(Bind Abbr) v t)))))))))))).(\lambda (H2: (sc3 g a1 c v)).(\lambda (w:
-T).(\lambda (H3: (sc3 g (asucc g a1) c w)).(let H4 \def H1 in (let TMP_60
-\def (Flat Appl) in (let TMP_61 \def (Bind Abbr) in (let TMP_62 \def (THead
-TMP_61 v t) in (let TMP_63 \def (THeads TMP_60 vs TMP_62) in (let TMP_64 \def
-(AHead a a0) in (let TMP_65 \def (arity g c TMP_63 TMP_64) in (let TMP_73
-\def (\forall (d: C).(\forall (w0: T).((sc3 g a d w0) \to (\forall (is:
-PList).((drop1 is d c) \to (let TMP_66 \def (Flat Appl) in (let TMP_67 \def
-(Flat Appl) in (let TMP_68 \def (Bind Abbr) in (let TMP_69 \def (THead TMP_68
-v t) in (let TMP_70 \def (THeads TMP_67 vs TMP_69) in (let TMP_71 \def (lift1
-is TMP_70) in (let TMP_72 \def (THead TMP_66 w0 TMP_71) in (sc3 g a0 d
-TMP_72))))))))))))) in (let TMP_74 \def (Flat Appl) in (let TMP_75 \def (Flat
-Appl) in (let TMP_76 \def (Bind Abst) in (let TMP_77 \def (THead TMP_76 w t)
-in (let TMP_78 \def (THead TMP_75 v TMP_77) in (let TMP_79 \def (THeads
-TMP_74 vs TMP_78) in (let TMP_80 \def (AHead a a0) in (let TMP_81 \def (arity
-g c TMP_79 TMP_80) in (let TMP_91 \def (\forall (d: C).(\forall (w0: T).((sc3
-g a d w0) \to (\forall (is: PList).((drop1 is d c) \to (let TMP_82 \def (Flat
-Appl) in (let TMP_83 \def (Flat Appl) in (let TMP_84 \def (Flat Appl) in (let
-TMP_85 \def (Bind Abst) in (let TMP_86 \def (THead TMP_85 w t) in (let TMP_87
-\def (THead TMP_84 v TMP_86) in (let TMP_88 \def (THeads TMP_83 vs TMP_87) in
-(let TMP_89 \def (lift1 is TMP_88) in (let TMP_90 \def (THead TMP_82 w0
-TMP_89) in (sc3 g a0 d TMP_90))))))))))))))) in (let TMP_92 \def (land TMP_81
-TMP_91) in (let TMP_225 \def (\lambda (H5: (arity g c (THeads (Flat Appl) vs
-(THead (Bind Abbr) v t)) (AHead a a0))).(\lambda (H6: ((\forall (d:
-C).(\forall (w0: T).((sc3 g a d w0) \to (\forall (is: PList).((drop1 is d c)
-\to (sc3 g a0 d (THead (Flat Appl) w0 (lift1 is (THeads (Flat Appl) vs (THead
-(Bind Abbr) v t)))))))))))).(let TMP_93 \def (Flat Appl) in (let TMP_94 \def
-(Flat Appl) in (let TMP_95 \def (Bind Abst) in (let TMP_96 \def (THead TMP_95
-w t) in (let TMP_97 \def (THead TMP_94 v TMP_96) in (let TMP_98 \def (THeads
-TMP_93 vs TMP_97) in (let TMP_99 \def (AHead a a0) in (let TMP_100 \def
-(arity g c TMP_98 TMP_99) in (let TMP_110 \def (\forall (d: C).(\forall (w0:
-T).((sc3 g a d w0) \to (\forall (is: PList).((drop1 is d c) \to (let TMP_101
-\def (Flat Appl) in (let TMP_102 \def (Flat Appl) in (let TMP_103 \def (Flat
-Appl) in (let TMP_104 \def (Bind Abst) in (let TMP_105 \def (THead TMP_104 w
-t) in (let TMP_106 \def (THead TMP_103 v TMP_105) in (let TMP_107 \def
-(THeads TMP_102 vs TMP_106) in (let TMP_108 \def (lift1 is TMP_107) in (let
-TMP_109 \def (THead TMP_101 w0 TMP_108) in (sc3 g a0 d TMP_109)))))))))))))))
-in (let TMP_111 \def (sc3_arity_gen g c v a1 H2) in (let TMP_112 \def (asucc
-g a1) in (let TMP_113 \def (sc3_arity_gen g c w TMP_112 H3) in (let TMP_114
-\def (AHead a a0) in (let TMP_115 \def (arity_appls_appl g c v a1 TMP_111 w
-TMP_113 t vs TMP_114 H5) in (let TMP_224 \def (\lambda (d: C).(\lambda (w0:
-T).(\lambda (H7: (sc3 g a d w0)).(\lambda (is: PList).(\lambda (H8: (drop1 is
-d c)).(let TMP_116 \def (Flat Appl) in (let TMP_117 \def (lifts1 is vs) in
-(let TMP_118 \def (Flat Appl) in (let TMP_119 \def (Bind Abst) in (let
-TMP_120 \def (THead TMP_119 w t) in (let TMP_121 \def (THead TMP_118 v
-TMP_120) in (let TMP_122 \def (lift1 is TMP_121) in (let TMP_123 \def (THeads
-TMP_116 TMP_117 TMP_122) in (let TMP_126 \def (\lambda (t0: T).(let TMP_124
-\def (Flat Appl) in (let TMP_125 \def (THead TMP_124 w0 t0) in (sc3 g a0 d
-TMP_125)))) in (let TMP_127 \def (Flat Appl) in (let TMP_128 \def (lift1 is
-v) in (let TMP_129 \def (Bind Abst) in (let TMP_130 \def (THead TMP_129 w t)
-in (let TMP_131 \def (lift1 is TMP_130) in (let TMP_132 \def (THead TMP_127
-TMP_128 TMP_131) in (let TMP_138 \def (\lambda (t0: T).(let TMP_133 \def
-(Flat Appl) in (let TMP_134 \def (Flat Appl) in (let TMP_135 \def (lifts1 is
-vs) in (let TMP_136 \def (THeads TMP_134 TMP_135 t0) in (let TMP_137 \def
-(THead TMP_133 w0 TMP_136) in (sc3 g a0 d TMP_137))))))) in (let TMP_139 \def
-(Bind Abst) in (let TMP_140 \def (lift1 is w) in (let TMP_141 \def (Ss is) in
-(let TMP_142 \def (lift1 TMP_141 t) in (let TMP_143 \def (THead TMP_139
-TMP_140 TMP_142) in (let TMP_152 \def (\lambda (t0: T).(let TMP_144 \def
-(Flat Appl) in (let TMP_145 \def (Flat Appl) in (let TMP_146 \def (lifts1 is
-vs) in (let TMP_147 \def (Flat Appl) in (let TMP_148 \def (lift1 is v) in
-(let TMP_149 \def (THead TMP_147 TMP_148 t0) in (let TMP_150 \def (THeads
-TMP_145 TMP_146 TMP_149) in (let TMP_151 \def (THead TMP_144 w0 TMP_150) in
-(sc3 g a0 d TMP_151)))))))))) in (let TMP_153 \def (lifts1 is vs) in (let
-TMP_154 \def (TCons w0 TMP_153) in (let H_y \def (H0 TMP_154) in (let TMP_155
-\def (lift1 is v) in (let TMP_156 \def (Ss is) in (let TMP_157 \def (lift1
-TMP_156 t) in (let TMP_158 \def (Bind Abbr) in (let TMP_159 \def (THead
-TMP_158 v t) in (let TMP_160 \def (lift1 is TMP_159) in (let TMP_166 \def
-(\lambda (t0: T).(let TMP_161 \def (Flat Appl) in (let TMP_162 \def (Flat
-Appl) in (let TMP_163 \def (lifts1 is vs) in (let TMP_164 \def (THeads
-TMP_162 TMP_163 t0) in (let TMP_165 \def (THead TMP_161 w0 TMP_164) in (sc3 g
-a0 d TMP_165))))))) in (let TMP_167 \def (Flat Appl) in (let TMP_168 \def
-(Bind Abbr) in (let TMP_169 \def (THead TMP_168 v t) in (let TMP_170 \def
-(THeads TMP_167 vs TMP_169) in (let TMP_171 \def (lift1 is TMP_170) in (let
-TMP_174 \def (\lambda (t0: T).(let TMP_172 \def (Flat Appl) in (let TMP_173
-\def (THead TMP_172 w0 t0) in (sc3 g a0 d TMP_173)))) in (let TMP_175 \def
-(H6 d w0 H7 is H8) in (let TMP_176 \def (Flat Appl) in (let TMP_177 \def
-(lifts1 is vs) in (let TMP_178 \def (Bind Abbr) in (let TMP_179 \def (THead
-TMP_178 v t) in (let TMP_180 \def (lift1 is TMP_179) in (let TMP_181 \def
-(THeads TMP_176 TMP_177 TMP_180) in (let TMP_182 \def (Bind Abbr) in (let
-TMP_183 \def (THead TMP_182 v t) in (let TMP_184 \def (lifts1_flat Appl is
-TMP_183 vs) in (let TMP_185 \def (eq_ind T TMP_171 TMP_174 TMP_175 TMP_181
-TMP_184) in (let TMP_186 \def (Bind Abbr) in (let TMP_187 \def (lift1 is v)
-in (let TMP_188 \def (Ss is) in (let TMP_189 \def (lift1 TMP_188 t) in (let
-TMP_190 \def (THead TMP_186 TMP_187 TMP_189) in (let TMP_191 \def (lift1_bind
-Abbr is v t) in (let TMP_192 \def (eq_ind T TMP_160 TMP_166 TMP_185 TMP_190
-TMP_191) in (let TMP_193 \def (sc3_lift1 g c a1 is d v H2 H8) in (let TMP_194
-\def (lift1 is w) in (let TMP_195 \def (asucc g a1) in (let TMP_196 \def
-(sc3_lift1 g c TMP_195 is d w H3 H8) in (let TMP_197 \def (H_y d TMP_155
-TMP_157 TMP_192 TMP_193 TMP_194 TMP_196) in (let TMP_198 \def (Bind Abst) in
-(let TMP_199 \def (THead TMP_198 w t) in (let TMP_200 \def (lift1 is TMP_199)
-in (let TMP_201 \def (lift1_bind Abst is w t) in (let TMP_202 \def (eq_ind_r
-T TMP_143 TMP_152 TMP_197 TMP_200 TMP_201) in (let TMP_203 \def (Flat Appl)
-in (let TMP_204 \def (Bind Abst) in (let TMP_205 \def (THead TMP_204 w t) in
-(let TMP_206 \def (THead TMP_203 v TMP_205) in (let TMP_207 \def (lift1 is
-TMP_206) in (let TMP_208 \def (Bind Abst) in (let TMP_209 \def (THead TMP_208
-w t) in (let TMP_210 \def (lift1_flat Appl is v TMP_209) in (let TMP_211 \def
-(eq_ind_r T TMP_132 TMP_138 TMP_202 TMP_207 TMP_210) in (let TMP_212 \def
-(Flat Appl) in (let TMP_213 \def (Flat Appl) in (let TMP_214 \def (Bind Abst)
-in (let TMP_215 \def (THead TMP_214 w t) in (let TMP_216 \def (THead TMP_213
-v TMP_215) in (let TMP_217 \def (THeads TMP_212 vs TMP_216) in (let TMP_218
-\def (lift1 is TMP_217) in (let TMP_219 \def (Flat Appl) in (let TMP_220 \def
-(Bind Abst) in (let TMP_221 \def (THead TMP_220 w t) in (let TMP_222 \def
-(THead TMP_219 v TMP_221) in (let TMP_223 \def (lifts1_flat Appl is TMP_222
-vs) in (eq_ind_r T TMP_123 TMP_126 TMP_211 TMP_218
-TMP_223)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-)))))))))))))))))))))) in (conj TMP_100 TMP_110 TMP_115
-TMP_224)))))))))))))))))) in (land_ind TMP_65 TMP_73 TMP_92 TMP_225
-H4)))))))))))))))))))))))))))))))) in (A_ind TMP_7 TMP_59 TMP_226 a2)))))).
+(asucc g a1) c w) \to (sc3 g a c (THeads (Flat Appl) vs (THead (Flat Appl) v
+(THead (Bind Abst) w t)))))))))))))).(\lambda (a0: A).(\lambda (H0: ((\forall
+(vs: TList).(\forall (c: C).(\forall (v: T).(\forall (t: T).((sc3 g a0 c
+(THeads (Flat Appl) vs (THead (Bind Abbr) v t))) \to ((sc3 g a1 c v) \to
+(\forall (w: T).((sc3 g (asucc g a1) c w) \to (sc3 g a0 c (THeads (Flat Appl)
+vs (THead (Flat Appl) v (THead (Bind Abst) w t)))))))))))))).(\lambda (vs:
+TList).(\lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (H1: (land
+(arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) (AHead a a0))
+(\forall (d: C).(\forall (w: T).((sc3 g a d w) \to (\forall (is:
+PList).((drop1 is d c) \to (sc3 g a0 d (THead (Flat Appl) w (lift1 is (THeads
+(Flat Appl) vs (THead (Bind Abbr) v t)))))))))))).(\lambda (H2: (sc3 g a1 c
+v)).(\lambda (w: T).(\lambda (H3: (sc3 g (asucc g a1) c w)).(let H4 \def H1
+in (land_ind (arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
+(AHead a a0)) (\forall (d: C).(\forall (w0: T).((sc3 g a d w0) \to (\forall
+(is: PList).((drop1 is d c) \to (sc3 g a0 d (THead (Flat Appl) w0 (lift1 is
+(THeads (Flat Appl) vs (THead (Bind Abbr) v t)))))))))) (land (arity g c
+(THeads (Flat Appl) vs (THead (Flat Appl) v (THead (Bind Abst) w t))) (AHead
+a a0)) (\forall (d: C).(\forall (w0: T).((sc3 g a d w0) \to (\forall (is:
+PList).((drop1 is d c) \to (sc3 g a0 d (THead (Flat Appl) w0 (lift1 is
+(THeads (Flat Appl) vs (THead (Flat Appl) v (THead (Bind Abst) w
+t)))))))))))) (\lambda (H5: (arity g c (THeads (Flat Appl) vs (THead (Bind
+Abbr) v t)) (AHead a a0))).(\lambda (H6: ((\forall (d: C).(\forall (w0:
+T).((sc3 g a d w0) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g a0 d
+(THead (Flat Appl) w0 (lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v
+t)))))))))))).(conj (arity g c (THeads (Flat Appl) vs (THead (Flat Appl) v
+(THead (Bind Abst) w t))) (AHead a a0)) (\forall (d: C).(\forall (w0:
+T).((sc3 g a d w0) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g a0 d
+(THead (Flat Appl) w0 (lift1 is (THeads (Flat Appl) vs (THead (Flat Appl) v
+(THead (Bind Abst) w t))))))))))) (arity_appls_appl g c v a1 (sc3_arity_gen g
+c v a1 H2) w (sc3_arity_gen g c w (asucc g a1) H3) t vs (AHead a a0) H5)
+(\lambda (d: C).(\lambda (w0: T).(\lambda (H7: (sc3 g a d w0)).(\lambda (is:
+PList).(\lambda (H8: (drop1 is d c)).(eq_ind_r T (THeads (Flat Appl) (lifts1
+is vs) (lift1 is (THead (Flat Appl) v (THead (Bind Abst) w t)))) (\lambda
+(t0: T).(sc3 g a0 d (THead (Flat Appl) w0 t0))) (eq_ind_r T (THead (Flat
+Appl) (lift1 is v) (lift1 is (THead (Bind Abst) w t))) (\lambda (t0: T).(sc3
+g a0 d (THead (Flat Appl) w0 (THeads (Flat Appl) (lifts1 is vs) t0))))
+(eq_ind_r T (THead (Bind Abst) (lift1 is w) (lift1 (Ss is) t)) (\lambda (t0:
+T).(sc3 g a0 d (THead (Flat Appl) w0 (THeads (Flat Appl) (lifts1 is vs)
+(THead (Flat Appl) (lift1 is v) t0))))) (let H_y \def (H0 (TCons w0 (lifts1
+is vs))) in (H_y d (lift1 is v) (lift1 (Ss is) t) (eq_ind T (lift1 is (THead
+(Bind Abbr) v t)) (\lambda (t0: T).(sc3 g a0 d (THead (Flat Appl) w0 (THeads
+(Flat Appl) (lifts1 is vs) t0)))) (eq_ind T (lift1 is (THeads (Flat Appl) vs
+(THead (Bind Abbr) v t))) (\lambda (t0: T).(sc3 g a0 d (THead (Flat Appl) w0
+t0))) (H6 d w0 H7 is H8) (THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead
+(Bind Abbr) v t))) (lifts1_flat Appl is (THead (Bind Abbr) v t) vs)) (THead
+(Bind Abbr) (lift1 is v) (lift1 (Ss is) t)) (lift1_bind Abbr is v t))
+(sc3_lift1 g c a1 is d v H2 H8) (lift1 is w) (sc3_lift1 g c (asucc g a1) is d
+w H3 H8))) (lift1 is (THead (Bind Abst) w t)) (lift1_bind Abst is w t))
+(lift1 is (THead (Flat Appl) v (THead (Bind Abst) w t))) (lift1_flat Appl is
+v (THead (Bind Abst) w t))) (lift1 is (THeads (Flat Appl) vs (THead (Flat
+Appl) v (THead (Bind Abst) w t)))) (lifts1_flat Appl is (THead (Flat Appl) v
+(THead (Bind Abst) w t)) vs)))))))))) H4)))))))))))))) a2))).