X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcnt%2Fprops.ma;h=e18a4788ea3109bee128a86e506e0ddce6d1b517;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=df42426cebbd66e004c9f21b85c002a3919eef90;hpb=8c62eb7de90e3c9a3a960fb0b3845bc561dddb75;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma
index df42426ce..e18a4788e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/cnt/props.ma
@@ -18,26 +18,17 @@ include "basic_1/cnt/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
- \lambda (t: T).(\lambda (H: (cnt t)).(let TMP_2 \def (\lambda (t0: 
-T).(\forall (i: nat).(\forall (d: nat).(let TMP_1 \def (lift i d t0) in (cnt 
-TMP_1))))) in (let TMP_9 \def (\lambda (n: nat).(\lambda (i: nat).(\lambda 
-(d: nat).(let TMP_3 \def (TSort n) in (let TMP_4 \def (\lambda (t0: T).(cnt 
-t0)) in (let TMP_5 \def (cnt_sort n) in (let TMP_6 \def (TSort n) in (let 
-TMP_7 \def (lift i d TMP_6) in (let TMP_8 \def (lift_sort n i d) in (eq_ind_r 
-T TMP_3 TMP_4 TMP_5 TMP_7 TMP_8)))))))))) in (let TMP_24 \def (\lambda (t0: 
+ \lambda (t: T).(\lambda (H: (cnt t)).(cnt_ind (\lambda (t0: T).(\forall (i: 
+nat).(\forall (d: nat).(cnt (lift i d t0))))) (\lambda (n: nat).(\lambda (i: 
+nat).(\lambda (d: nat).(eq_ind_r T (TSort n) (\lambda (t0: T).(cnt t0)) 
+(cnt_sort n) (lift i d (TSort n)) (lift_sort n i d))))) (\lambda (t0: 
 T).(\lambda (_: (cnt t0)).(\lambda (H1: ((\forall (i: nat).(\forall (d: 
 nat).(cnt (lift i d t0)))))).(\lambda (k: K).(\lambda (v: T).(\lambda (i: 
-nat).(\lambda (d: nat).(let TMP_10 \def (lift i d v) in (let TMP_11 \def (s k 
-d) in (let TMP_12 \def (lift i TMP_11 t0) in (let TMP_13 \def (THead k TMP_10 
-TMP_12) in (let TMP_14 \def (\lambda (t1: T).(cnt t1)) in (let TMP_15 \def (s 
-k d) in (let TMP_16 \def (lift i TMP_15 t0) in (let TMP_17 \def (s k d) in 
-(let TMP_18 \def (H1 i TMP_17) in (let TMP_19 \def (lift i d v) in (let 
-TMP_20 \def (cnt_head TMP_16 TMP_18 k TMP_19) in (let TMP_21 \def (THead k v 
-t0) in (let TMP_22 \def (lift i d TMP_21) in (let TMP_23 \def (lift_head k v 
-t0 i d) in (eq_ind_r T TMP_13 TMP_14 TMP_20 TMP_22 
-TMP_23)))))))))))))))))))))) in (cnt_ind TMP_2 TMP_9 TMP_24 t H))))).
+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)).