\lambda (g: G).(\lambda (a: A).(\lambda (c: C).(\lambda (t: T).(\lambda (H:
(sc3 g a c t)).(let H_x \def (sc3_props__sc3_sn3_abst g a) in (let H0 \def
H_x in (land_ind (\forall (c0: C).(\forall (t0: T).((sc3 g a c0 t0) \to (sn3
-c0 t0)))) (\forall (vs: TList).(\forall (i: nat).(let t0 \def (THeads (Flat
-Appl) vs (TLRef i)) in (\forall (c0: C).((arity g c0 t0 a) \to ((nf2 c0
-(TLRef i)) \to ((sns3 c0 vs) \to (sc3 g a c0 t0)))))))) (sn3 c t) (\lambda
-(H1: ((\forall (c0: C).(\forall (t0: T).((sc3 g a c0 t0) \to (sn3 c0
-t0)))))).(\lambda (_: ((\forall (vs: TList).(\forall (i: nat).(let t0 \def
-(THeads (Flat Appl) vs (TLRef i)) in (\forall (c0: C).((arity g c0 t0 a) \to
-((nf2 c0 (TLRef i)) \to ((sns3 c0 vs) \to (sc3 g a c0 t0)))))))))).(H1 c t
-H))) H0))))))).
+c0 t0)))) (\forall (vs: TList).(\forall (i: nat).(\forall (c0: C).((arity g
+c0 (THeads (Flat Appl) vs (TLRef i)) a) \to ((nf2 c0 (TLRef i)) \to ((sns3 c0
+vs) \to (sc3 g a c0 (THeads (Flat Appl) vs (TLRef i))))))))) (sn3 c t)
+(\lambda (H1: ((\forall (c0: C).(\forall (t0: T).((sc3 g a c0 t0) \to (sn3 c0
+t0)))))).(\lambda (_: ((\forall (vs: TList).(\forall (i: nat).(\forall (c0:
+C).((arity g c0 (THeads (Flat Appl) vs (TLRef i)) a) \to ((nf2 c0 (TLRef i))
+\to ((sns3 c0 vs) \to (sc3 g a c0 (THeads (Flat Appl) vs (TLRef
+i))))))))))).(H1 c t H))) H0))))))).
theorem sc3_abst:
\forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall
a)).(\lambda (H0: (nf2 c (TLRef i))).(\lambda (H1: (sns3 c vs)).(let H_x \def
(sc3_props__sc3_sn3_abst g a) in (let H2 \def H_x in (land_ind (\forall (c0:
C).(\forall (t: T).((sc3 g a c0 t) \to (sn3 c0 t)))) (\forall (vs0:
-TList).(\forall (i0: nat).(let t \def (THeads (Flat Appl) vs0 (TLRef i0)) in
-(\forall (c0: C).((arity g c0 t a) \to ((nf2 c0 (TLRef i0)) \to ((sns3 c0
-vs0) \to (sc3 g a c0 t)))))))) (sc3 g a c (THeads (Flat Appl) vs (TLRef i)))
-(\lambda (_: ((\forall (c0: C).(\forall (t: T).((sc3 g a c0 t) \to (sn3 c0
-t)))))).(\lambda (H4: ((\forall (vs0: TList).(\forall (i0: nat).(let t \def
-(THeads (Flat Appl) vs0 (TLRef i0)) in (\forall (c0: C).((arity g c0 t a) \to
-((nf2 c0 (TLRef i0)) \to ((sns3 c0 vs0) \to (sc3 g a c0 t)))))))))).(H4 vs i
-c H H0 H1))) H2)))))))))).
+TList).(\forall (i0: nat).(\forall (c0: C).((arity g c0 (THeads (Flat Appl)
+vs0 (TLRef i0)) a) \to ((nf2 c0 (TLRef i0)) \to ((sns3 c0 vs0) \to (sc3 g a
+c0 (THeads (Flat Appl) vs0 (TLRef i0))))))))) (sc3 g a c (THeads (Flat Appl)
+vs (TLRef i))) (\lambda (_: ((\forall (c0: C).(\forall (t: T).((sc3 g a c0 t)
+\to (sn3 c0 t)))))).(\lambda (H4: ((\forall (vs0: TList).(\forall (i0:
+nat).(\forall (c0: C).((arity g c0 (THeads (Flat Appl) vs0 (TLRef i0)) a) \to
+((nf2 c0 (TLRef i0)) \to ((sns3 c0 vs0) \to (sc3 g a c0 (THeads (Flat Appl)
+vs0 (TLRef i0))))))))))).(H4 vs i c H H0 H1))) H2)))))))))).
theorem sc3_bind:
\forall (g: G).(\forall (b: B).((not (eq B b Abst)) \to (\forall (a1: