X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_lreq.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_lreq.ma;h=7059e9c431af0a77eb521dbb0b503de37b4cb6b4;hb=6555775aa5268dec0d9ae4579412b659cacdc964;hp=c9934f66450fd0686db6bdc11e79e66d2f7d3492;hpb=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
index c9934f664..7059e9c43 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
@@ -19,9 +19,9 @@ include "basic_2/relocation/drops_lexs.ma".
 
 (* Properties with ranged equivalence for local environments ****************)
 
-lemma lreq_co_dedropable: co_dedropable_sn lreq.
-@lexs_liftable_co_dedropable
-/2 width=6 by cfull_lift, ceq_lift/ qed-.
+lemma lreq_co_dedropable_sn: co_dedropable_sn lreq.
+@lexs_liftable_co_dedropable_sn
+/2 width=6 by cfull_lift_sn, ceq_lift_sn/ qed-.
 
 lemma lreq_co_dropable_sn: co_dropable_sn lreq.
 @lexs_co_dropable_sn qed-.
@@ -55,4 +55,4 @@ lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 →
                              ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
 #f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
-/2 width=6 by cfull_lift, ceq_lift, ex3_intro/ qed-.
+/2 width=6 by cfull_lift_sn, ceq_lift_sn, ex3_intro/ qed-.