X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts.ma;h=6a66289bd6f28f6e56ad0222650fc5bb080d59f7;hb=46815bb7af06b235ead2fd67a4aee2d294b51928;hp=0ca46fa3c40120ad5e70fc5917055f1f4205c5cf;hpb=952ec5aa2e9a54787acb63a5c8d6fdbf9011ab60;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index 0ca46fa3c..6a66289bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -16,7 +16,7 @@ include "ground_2/relocation/trace_isid.ma".
 include "basic_2/notation/relations/rliftstar_3.ma".
 include "basic_2/grammar/term.ma".
 
-(* GENERIC TERM RELOCATION **************************************************)
+(* GENERIC RELOCATION FOR TERMS *********************************************)
 
 (* Basic_1: includes:
             lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
@@ -334,11 +334,11 @@ lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2).
 ]
 qed-.
 
-(* Basic_2A1: removed theorems 17:
-              lifts_inv_nil lifts_inv_cons lifts_total
+(* Basic_2A1: removed theorems 14:
+              lifts_inv_nil lifts_inv_cons
               lift_inv_Y1 lift_inv_Y2 lift_inv_lref_Y1 lift_inv_lref_Y2 lift_lref_Y lift_Y1
               lift_lref_lt_eq lift_lref_ge_eq lift_lref_plus lift_lref_pred
-              lift_lref_ge_minus lift_lref_ge_minus_eq lift_total lift_refl
+              lift_lref_ge_minus lift_lref_ge_minus_eq
 *)
 (* Basic_1: removed theorems 8:
             lift_lref_gt