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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cnt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cnt/props.ma
index 2185c5a8f..7fcd315eb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cnt/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cnt/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/cnt/defs.ma".
+include "Basic-1/cnt/defs.ma".
 
-include "LambdaDelta-1/lift/fwd.ma".
+include "Basic-1/lift/fwd.ma".
 
 theorem cnt_lift:
  \forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i 
@@ -31,4 +31,7 @@ nat).(cnt (lift i d t0)))))).(\lambda (k: K).(\lambda (v: T).(\lambda (i:
 nat).(\lambda (d: nat).(eq_ind_r T (THead k (lift i d v) (lift i (s k d) t0)) 
 (\lambda (t1: T).(cnt t1)) (cnt_head (lift i (s k d) t0) (H1 i (s k d)) k 
 (lift i d v)) (lift i d (THead k v t0)) (lift_head k v t0 i d))))))))) t H)).
+(* COMMENTS
+Initial nodes: 191
+END *)