X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsty0%2Fprops.ma;h=00c9f68185b08fc9d46dea5cfa44eff29c2ffd1e;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=7709a86977957acd985c745e4d3ae7038000f1b4;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/props.ma
index 7709a8697..00c9f6818 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sty0/defs.ma".
+include "Basic-1/sty0/defs.ma".
 
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
 
 theorem sty0_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e 
@@ -159,6 +159,9 @@ h d H4) (lift h (s (Flat Cast) d) t3) (lift h (s (Flat Cast) d) t4) (H3 c0 h
 (s (Flat Cast) d) H4)) (lift h d (THead (Flat Cast) v2 t4)) (lift_head (Flat 
 Cast) v2 t4 h d)) (lift h d (THead (Flat Cast) v1 t3)) (lift_head (Flat Cast) 
 v1 t3 h d))))))))))))))) e t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 3677
+END *)
 
 theorem sty0_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c 
@@ -208,4 +211,7 @@ T).(sty0 g c0 (THead (Flat Cast) v2 t3) t4))) (\lambda (x0: T).(\lambda (H7:
 (sty0 g c0 t3 x0)).(ex_intro T (\lambda (t4: T).(sty0 g c0 (THead (Flat Cast) 
 v2 t3) t4)) (THead (Flat Cast) x x0) (sty0_cast g c0 v2 x H5 t3 x0 H7)))) 
 H6)))) H4))))))))))) c t1 t H))))).
+(* COMMENTS
+Initial nodes: 991
+END *)