update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / csubc / csuba.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubc/csuba.ma b/matita/matita/contribs/lambdadelta/basic_1/csubc/csuba.ma
index 2abfe2a1f5f0da4396f92062e6db6da842859d2b..9e1d3014eafb585ea8f679b0ce20e20c2149a594 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/csubc/csuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubc/csuba.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/csubc/defs.ma".
+include "basic_1/csubc/fwd.ma".
 
-include "Basic-1/sc3/props.ma".
+include "basic_1/sc3/props.ma".
 
-theorem csubc_csuba:
+lemma csubc_csuba:
  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((csubc g c1 c2) \to (csuba 
 g c1 c2))))
 \def
@@ -34,7 +34,4 @@ C).(\lambda (_: (csubc g c3 c4)).(\lambda (H1: (csuba g c3 c4)).(\lambda (v:
 T).(\lambda (a: A).(\lambda (H2: (sc3 g (asucc g a) c3 v)).(\lambda (w: 
 T).(\lambda (H3: (sc3 g a c4 w)).(csuba_abst g c3 c4 H1 v a (sc3_arity_gen g 
 c3 v (asucc g a) H2) w (sc3_arity_gen g c4 w a H3))))))))))) c1 c2 H)))).
-(* COMMENTS
-Initial nodes: 231
-END *)