dependences update

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / sty1 / cnt.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty1/cnt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty1/cnt.ma
index f5d71c1d083197ae8a14b6ab19547fea917997c8..0f39bdfd93b0cbdc61159f871bef58435c3f8496 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty1/cnt.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty1/cnt.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sty1/props.ma".
+include "Basic-1/sty1/props.ma".
 
-include "LambdaDelta-1/cnt/props.ma".
+include "Basic-1/cnt/props.ma".
 
 theorem sty1_cnt:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c 
@@ -83,4 +83,7 @@ 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 *)