update in basic_2 and ground_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
index 5310d8ab791aac77a0b133907090ed8a605fee55..b34b79890ee395333c857db28138b50fd15ee605 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
@@ -44,7 +44,7 @@ qed.
 
 (* Basic_2A1: uses: lsx_lref_be *)
 lemma lfsx_lref_pair_drops: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
-                            â\88\80I,i,L. â¬\87*[i] L â\89¡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+                            â\88\80I,i,L. â¬\87*[i] L â\89\98 K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
 #h #o #G #K #V #HV #HK #I #i elim i -i
 [ #L #H >(drops_fwd_isid … H) -H /2 width=3 by lfsx_pair_lpxs/
 | #i #IH #L #H