notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / llpx_sn_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
index 126b733215b7d363ef1094a256172b5b9cd81657..956ae4699a22724b2b878425a51ed28792a86be3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
@@ -21,7 +21,7 @@ include "basic_2/multiple/llpx_sn_alt_rec.ma".
 definition llpx_sn_alt: relation3 lenv term term → relation4 ynat term lenv lenv ≝
                         λR,d,T,L1,L2. |L1| = |L2| ∧
                         (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ →
-                           â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+                           â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
                            I1 = I2 ∧ R K1 V1 V2
                         ).