X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frsx_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frsx_drops.ma;h=64ebcd6669b08b2a5f4dda0c539bbf47b367ff85;hb=f76594123e375bd7852c9421fe260a7bec693a92;hp=80cc2f1f74669726d69d99e9dfdb45eda9d981c3;hpb=a454837a256907d2f83d42ced7be847e10361ea9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
index 80cc2f1f7..64ebcd666 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
@@ -43,13 +43,13 @@ qed-.
 (* Advanced properties ******************************************************)
 
 (* Basic_2A1: uses: lsx_lref_free *)
-lemma rsx_lref_atom (h) (G): ∀L,i. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
+lemma rsx_lref_atom_drops (h) (G): ∀L,i. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
 #h #G #L1 #i #HL1
 @(rsx_lifts … (#0) … HL1) -HL1 //
 qed.
 
 (* Basic_2A1: uses: lsx_lref_skip *)
-lemma rsx_lref_unit (h) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
+lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
 #h #G #I #L1 #K1 #i #HL1
 @(rsx_lifts … (#0) … HL1) -HL1 //
 qed.
@@ -57,7 +57,7 @@ qed.
 (* Advanced forward lemmas **************************************************)
 
 (* Basic_2A1: uses: lsx_fwd_lref_be *)
-lemma rsx_fwd_lref_pair (h) (G):
+lemma rsx_fwd_lref_pair_drops (h) (G):
       ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
       ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
 #h #G #L #i #HL #I #K #V #HLK