X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfsx_drops.ma;h=488bb09ccce9a4355ecb1f64ba4cd4893295c667;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=e4679904febe746438a9c4d017bcb877fffea566;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma
index e4679904f..488bb09cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma
@@ -44,13 +44,13 @@ qed-.
 (* Advanced properties ******************************************************)
 
 (* Basic_2A1: uses: lsx_lref_free *)
-lemma lfsx_lref_atom: ∀h,o,G,L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+lemma lfsx_lref_atom: ∀h,o,G,L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
 #h #o #G #L1 #i #HL1
 @(lfsx_lifts … (#0) … HL1) -HL1 //
 qed.
 
 (* Basic_2A1: uses: lsx_lref_skip *)
-lemma lfsx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≡ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+lemma lfsx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
 #h #o #I #G #L1 #K1 #i #HL1
 @(lfsx_lifts … (#0) … HL1) -HL1 //
 qed.
@@ -59,7 +59,7 @@ qed.
 
 (* Basic_2A1: uses: lsx_fwd_lref_be *)
 lemma lfsx_fwd_lref_pair: ∀h,o,G,L,i. G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄ →
-                          ∀I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+                          ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
 #h #o #G #L #i #HL #I #K #V #HLK
 lapply (lfsx_inv_lifts … HL … HLK … (#0) ?) -L
 /2 width=2 by lfsx_fwd_pair/