- revision of ground_2 and basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
index 848284a25f615e03486ef24b60f4f11de64e1088..59cddfbc9178a6cac9368afb928c42b28ddb3f4e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
@@ -32,7 +32,7 @@ lemma cpys_subst: ∀I,G,L,K,V,U1,i,l,m.
   lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
   lapply (cpy_weak … HU02 l m ? ?) -HU02
   [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
-  >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/
+  >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ1/
 ]
 qed.
 
@@ -61,7 +61,7 @@ lemma cpys_inv_atom1: ∀I,G,L,T2,l,m. ⦃G, L⦄ ⊢ ⓪{I} ▶*[l, m] T2 →
   | * #J #K #V1 #V #i #Hli #Hilm #HLK #HV1 #HVT #HI
     lapply (drop_fwd_drop2 … HLK) #H
     elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
-    [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
+    [2,3,4: /2 width=1 by ylt_fwd_le_succ1, yle_succ_dx/ ]
     /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
   ]
 ]
@@ -92,7 +92,7 @@ lemma cpys_inv_lref1_drop: ∀G,L,T2,i,l,m. ⦃G, L⦄ ⊢ #i ▶*[l, m] T2 →
                              & l ≤ i
                              & i < l + m.
 #G #L #T2 #i #l #m #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
-[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK //
+[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK /2 width=1 by ylt_inj/
 | * #Z #Y #X1 #X2 #Hli #Hilm #HLY #HX12 #HXT2
   lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
   lapply (drop_mono … HLY … HLK) -L #H destruct
@@ -103,7 +103,7 @@ qed-.
 (* Properties on relocation *************************************************)
 
 lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
-                    ∀L,U1,s,l,m. lt + mt ≤ yinj l → ⬇[s, l, m] L ≡ K →
+                    ∀L,U1,s,l,m. lt + mt ≤ l → ⬇[s, l, m] L ≡ K →
                     ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
                     ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2.
 #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hlmtl #HLK #HTU1 @(cpys_ind … H) -T2
@@ -116,7 +116,7 @@ lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
 qed-.
 
 lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
-                    ∀L,U1,s,l,m. lt ≤ yinj l → l ≤ lt + mt →
+                    ∀L,U1,s,l,m. lt ≤ l → l ≤ lt + mt →
                     ⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 →
                     ∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt, mt + m] U2.
 #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hltl #Hllmt #HLK #HTU1 @(cpys_ind … H) -T2
@@ -129,7 +129,7 @@ lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
 qed-.
 
 lemma cpys_lift_ge: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
-                    ∀L,U1,s,l,m. yinj l ≤ lt → ⬇[s, l, m] L ≡ K →
+                    ∀L,U1,s,l,m. l ≤ lt → ⬇[s, l, m] L ≡ K →
                     ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
                     ⦃G, L⦄ ⊢ U1 ▶*[lt+m, mt] U2.
 #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hllt #HLK #HTU1 @(cpys_ind … H) -T2
@@ -156,7 +156,7 @@ qed-.
 
 lemma cpys_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
                          ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
-                         lt ≤ l → yinj l + m ≤ lt + mt →
+                         lt ≤ l → l + m ≤ lt + mt →
                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt - m] T2 & ⬆[l, m] T2 ≡ U2.
 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmlmt @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
@@ -167,7 +167,7 @@ qed-.
 
 lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
                          ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
-                         yinj l + m ≤ lt →
+                         l + m ≤ lt →
                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt - m, mt] T2 & ⬆[l, m] T2 ≡ U2.
 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmlt @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
@@ -180,8 +180,8 @@ qed-.
 
 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
                             ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
-                            l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt →
-                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (yinj l + m)] T2 &
+                            l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (l + m)] T2 &
                                  ⬆[l, m] T2 ≡ U2.
 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
@@ -192,7 +192,7 @@ qed-.
 
 lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
                             ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
-                            lt ≤ l → lt + mt ≤ yinj l + m →
+                            lt ≤ l → lt + mt ≤ l + m →
                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
@@ -203,7 +203,7 @@ qed-.
 
 lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
                             ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
-                            lt ≤ l → l ≤ lt + mt → lt + mt ≤ yinj l + m →
+                            lt ≤ l → l ≤ lt + mt → lt + mt ≤ l + m →
                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
 #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
@@ -213,7 +213,7 @@ lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U
 qed-.
 
 lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,l,m. ⦃G, L⦄ ⊢ W1 ▶*[l, m] W2 →
-                            ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 → 
+                            ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 →
                             l ≤ yinj i → i < l + m →
                             ∃∃V2.  ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(l+m-i)] V2 & ⬆[O, i+1] V2 ≡ W2.
 #G #L #W1 #W2 #l #m #HW12 #K #V1 #i #HLK #HVW1 #Hli #Hilm