update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / cnt / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma
index 7fcd315eb06850af47b7b74b7482fd04c22fdc5e..e18a4788ea3109bee128a86e506e0ddce6d1b517 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/cnt/defs.ma".
+include "basic_1/cnt/fwd.ma".
 
-include "Basic-1/lift/fwd.ma".
+include "basic_1/lift/props.ma".
 
-theorem cnt_lift:
+lemma cnt_lift:
  \forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i 
 d t)))))
 \def
@@ -31,7 +31,4 @@ 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 *)