very very interesting hack

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / sc3 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma
index d63d5e3cd45cfc2d43a2ac4418d967b855abf9ae..cd5ce1f7d42e880cd8a98e2cc4c35e211e57c277 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma
@@ -505,14 +505,14 @@ t) \to (sn3 c t)))))
  \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 
@@ -524,14 +524,14 @@ i)) \to ((sns3 c vs) \to (sc3 g a c (THeads (Flat Appl) vs (TLRef i))))))))))
 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: