X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flleq_alt_rec.ma;h=692ece149c1a928433a324e411dacf00c78903ad;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=b8646bc0e63788f1d47ef58b78d9d86d8ccfd27d;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

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 b8646bc0e..692ece149 100644
--- 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| →
-                          (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                             ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                          (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⬆[i, 1] U ≡ T → ⊥) →
+                             ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[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| → (
-                           ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                           ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⬆[i, 1] U ≡ T → ⊥) →
+                           ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[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| ∧
-                        ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                        ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                        ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⬆[i, 1] U ≡ T → ⊥) →
+                        ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[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 //