notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt.ma
index 38b34aec57916bc41c2e6b70744c2afeae0d8a1f..2c6b8feb6178752145f8b17b46ae2e502864c934 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt.ma
@@ -21,7 +21,7 @@ include "basic_2/multiple/lleq.ma".
 
 theorem lleq_intro_alt: ∀L1,L2,T,d. |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 ∧ V1 = V2
                         ) → L1 ≡[T, d] L2.
 #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_inv_llpx_sn @conj // -HL12
@@ -32,7 +32,7 @@ qed.
 theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ≡[T, d] 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 ∧ V1 = V2.
 #L1 #L2 #T #d #H elim (llpx_sn_llpx_sn_alt … H) -H
 #HL12 #IH @conj //