notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt_rec.ma
index b8646bc0e63788f1d47ef58b78d9d86d8ccfd27d..692ece149c1a928433a324e411dacf00c78903ad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt_rec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt_rec.ma
@@ -20,8 +20,8 @@ include "basic_2/multiple/lleq.ma".
 (* Alternative definition (recursive) ***************************************)
 
 theorem lleq_intro_alt_r: ∀L1,L2,T,d. |L1| = |L2| →
-                          (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
-                             â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+                          (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+                             â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
                              ∧∧ I1 = I2 & V1 = V2 & K1 ≡[V1, 0] K2
                           ) → L1 ≡[T, d] L2.
 #L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt_r // -HL12
@@ -31,8 +31,8 @@ qed.
 
 theorem lleq_ind_alt_r: ∀S:relation4 ynat term lenv lenv.
                         (∀L1,L2,T,d. |L1| = |L2| → (
-                           â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
-                           â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+                           â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+                           â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
                            ∧∧ I1 = I2 & V1 = V2 & K1 ≡[V1, 0] K2 & S 0 V1 K1 K2
                         ) → S d T L1 L2) →
                         ∀L1,L2,T,d. L1 ≡[T, d] L2 → S d T L1 L2.
@@ -44,8 +44,8 @@ qed-.
 
 theorem lleq_inv_alt_r: ∀L1,L2,T,d. L1 ≡[T, d] L2 →
                         |L1| = |L2| ∧
-                        â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
-                        â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+                        â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+                        â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
                         ∧∧ I1 = I2 & V1 = V2 & K1 ≡[V1, 0] K2.
 #L1 #L2 #T #d #H elim (llpx_sn_inv_alt_r … H) -H
 #HL12 #IH @conj //