universary milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsx_drop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_drop.ma
index f1a4c7b64e8f4ed33d7eb8487a08a7552a577aa4..c70d6fbc585966777eadc0270063b8932245a215 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_drop.ma
@@ -20,23 +20,23 @@ include "basic_2/computation/lsx.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma lsx_lref_free: ∀h,g,G,L,l,i. |L| ≤ i → G ⊢ ⬊*[h, g, #i, l] L.
-#h #g #G #L1 #l #i #HL1 @lsx_intro
+lemma lsx_lref_free: ∀h,o,G,L,l,i. |L| ≤ i → G ⊢ ⬊*[h, o, #i, l] L.
+#h #o #G #L1 #l #i #HL1 @lsx_intro
 #L2 #HL12 #H elim H -H
 /4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/
 qed.
 
-lemma lsx_lref_skip: ∀h,g,G,L,l,i. yinj i < l → G ⊢ ⬊*[h, g, #i, l] L.
-#h #g #G #L1 #l #i #HL1 @lsx_intro
+lemma lsx_lref_skip: ∀h,o,G,L,l,i. yinj i < l → G ⊢ ⬊*[h, o, #i, l] L.
+#h #o #G #L1 #l #i #HL1 @lsx_intro
 #L2 #HL12 #H elim H -H
 /3 width=4 by lpx_fwd_length, lleq_skip/
 qed.
 
 (* Advanced forward lemmas **************************************************)
 
-lemma lsx_fwd_lref_be: ∀h,g,I,G,L,l,i. l ≤ yinj i → G ⊢ ⬊*[h, g, #i, l] L →
-                       ∀K,V. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, V, 0] K.
-#h #g #I #G #L #l #i #Hli #H @(lsx_ind … H) -L
+lemma lsx_fwd_lref_be: ∀h,o,I,G,L,l,i. l ≤ yinj i → G ⊢ ⬊*[h, o, #i, l] L →
+                       ∀K,V. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, V, 0] K.
+#h #o #I #G #L #l #i #Hli #H @(lsx_ind … H) -L
 #L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
 #K2 #HK12 #HnK12 lapply (drop_fwd_drop2 … HLK1)
 #H2LK1 elim (drop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12
@@ -48,19 +48,19 @@ qed-.
 
 (* Properties on relocation *************************************************)
 
-lemma lsx_lift_le: ∀h,g,G,K,T,U,lt,l,m. lt ≤ yinj l →
-                   ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, T, lt] K →
-                   ∀L. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, U, lt] L.
-#h #g #G #K #T #U #lt #l #m #Hltl #HTU #H @(lsx_ind … H) -K
+lemma lsx_lift_le: ∀h,o,G,K,T,U,lt,l,k. lt ≤ yinj l →
+                   ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, T, lt] K →
+                   ∀L. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, U, lt] L.
+#h #o #G #K #T #U #lt #l #k #Hltl #HTU #H @(lsx_ind … H) -K
 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
 #L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12
 /4 width=10 by lleq_lift_le/
 qed-.
 
-lemma lsx_lift_ge: ∀h,g,G,K,T,U,lt,l,m. yinj l ≤ lt →
-                   ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, T, lt] K →
-                   ∀L. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, U, lt + m] L.
-#h #g #G #K #T #U #lt #l #m #Hllt #HTU #H @(lsx_ind … H) -K
+lemma lsx_lift_ge: ∀h,o,G,K,T,U,lt,l,k. yinj l ≤ lt →
+                   ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, T, lt] K →
+                   ∀L. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, U, lt + k] L.
+#h #o #G #K #T #U #lt #l #k #Hllt #HTU #H @(lsx_ind … H) -K
 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
 #L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12
 /4 width=9 by lleq_lift_ge/
@@ -68,28 +68,28 @@ qed-.
 
 (* Inversion lemmas on relocation *******************************************)
 
-lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,lt,l,m. lt ≤ yinj l →
-                       ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
-                       ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, lt] K.
-#h #g #G #L #T #U #lt #l #m #Hltl #HTU #H @(lsx_ind … H) -L
+lemma lsx_inv_lift_le: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l →
+                       ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L →
+                       ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, lt] K.
+#h #o #G #L #T #U #lt #l #k #Hltl #HTU #H @(lsx_ind … H) -L
 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
 #K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
 /4 width=10 by lleq_inv_lift_le/
 qed-.
 
-lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,lt,l,m. yinj l ≤ lt → lt ≤ l + m →
-                       ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
-                       ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, l] K.
-#h #g #G #L #T #U #lt #l #m #Hllt #Hltlm #HTU #H @(lsx_ind … H) -L
+lemma lsx_inv_lift_be: ∀h,o,G,L,T,U,lt,l,k. yinj l ≤ lt → lt ≤ l + k →
+                       ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L →
+                       ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, l] K.
+#h #o #G #L #T #U #lt #l #k #Hllt #Hltlm #HTU #H @(lsx_ind … H) -L
 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
 #K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
 /4 width=11 by lleq_inv_lift_be/
 qed-.
 
-lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,lt,l,m. yinj l + yinj m ≤ lt →
-                       ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
-                       ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, lt-m] K.
-#h #g #G #L #T #U #lt #l #m #Hlmlt #HTU #H @(lsx_ind … H) -L
+lemma lsx_inv_lift_ge: ∀h,o,G,L,T,U,lt,l,k. yinj l + yinj k ≤ lt →
+                       ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L →
+                       ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, lt-k] K.
+#h #o #G #L #T #U #lt #l #k #Hlmlt #HTU #H @(lsx_ind … H) -L
 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
 #K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
 /4 width=9 by lleq_inv_lift_ge/