update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lfsx_drops.ma

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 e4679904febe746438a9c4d017bcb877fffea566..488bb09ccce9a4355ecb1f64ba4cd4893295c667 100644 (file)
--- 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: â\88\80h,o,G,L,i. â¬\87*[â\92», ð\9d\90\94â\9d´iâ\9dµ] L â\89¡ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+lemma lfsx_lref_atom: â\88\80h,o,G,L,i. â¬\87*[â\92», ð\9d\90\94â\9d´iâ\9dµ] L â\89\98 ⋆ → 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: â\88\80h,o,I,G,L,K,i. â¬\87*[i] L â\89¡ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+lemma lfsx_lref_unit: â\88\80h,o,I,G,L,K,i. â¬\87*[i] L â\89\98 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⦄ →
-                          â\88\80I,K,V. â¬\87*[i] L â\89¡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+                          â\88\80I,K,V. â¬\87*[i] L â\89\98 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/