X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsc3%2Farity.ma;h=651321580bc49142be0b0fec975be1c0e3339426;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=b84dc67bd865a471f48f46a7bddaa6bab0f45704;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/arity.ma
index b84dc67bd..651321580 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/arity.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubc/arity.ma".
+include "Basic-1/csubc/arity.ma".
 
-include "LambdaDelta-1/csubc/getl.ma".
+include "Basic-1/csubc/getl.ma".
 
-include "LambdaDelta-1/csubc/drop1.ma".
+include "Basic-1/csubc/drop1.ma".
 
-include "LambdaDelta-1/csubc/props.ma".
+include "Basic-1/csubc/props.ma".
 
 theorem sc3_arity_csubc:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
@@ -305,6 +305,9 @@ d1 c2) \to (sc3 g a1 c2 (lift1 is t0))))))))).(\lambda (a2: A).(\lambda (H2:
 (leq g a1 a2)).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H3: (drop1 is 
 d1 c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(sc3_repl g a1 c2 
 (lift1 is t0) (H1 d1 is H3 c2 H4) a2 H2))))))))))))) c1 t a H))))).
+(* COMMENTS
+Initial nodes: 5940
+END *)
 
 theorem sc3_arity:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t 
@@ -313,4 +316,7 @@ a) \to (sc3 g a c t)))))
  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H: 
 (arity g c t a)).(let H_y \def (sc3_arity_csubc g c t a H c PNil) in (H_y 
 (drop1_nil c) c (csubc_refl g c))))))).
+(* COMMENTS
+Initial nodes: 47
+END *)