- advances towards strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_lreq.ma

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 c9934f66450fd0686db6bdc11e79e66d2f7d3492..7059e9c431af0a77eb521dbb0b503de37b4cb6b4 100644 (file)
--- 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-.