X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsty1%2Fcnt.ma;h=54354378cd5c6677f8029556bdb11c4e22af5dd1;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=0f39bdfd93b0cbdc61159f871bef58435c3f8496;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma
index 0f39bdfd9..54354378c 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty1/props.ma".
+include "basic_1/sty1/props.ma".
 
-include "Basic-1/cnt/props.ma".
+include "basic_1/cnt/props.ma".
 
-theorem sty1_cnt:
+lemma sty1_cnt:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c 
 t1 t) \to (ex2 T (\lambda (t2: T).(sty1 g c t1 t2)) (\lambda (t2: T).(cnt 
 t2)))))))
@@ -83,7 +83,4 @@ x0)).(\lambda (H9: (sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat Cast) x0
 x))).(ex_intro2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Cast) v1 t2) t4)) 
 (\lambda (t4: T).(cnt t4)) (THead (Flat Cast) x0 x) H9 (cnt_head x H6 (Flat 
 Cast) x0))))) H7)))))) H4))))))))))) c t1 t H))))).
-(* COMMENTS
-Initial nodes: 1313
-END *)