- ng_refiner:

[helm.git] / matita / matita / contribs / lambda / subterms / relocation.ma

diff --git a/matita/matita/contribs/lambda/subterms/relocation.ma b/matita/matita/contribs/lambda/subterms/relocation.ma
index 5f64efc93e363a9eda7cc7b140c0374d70a401c7..0943d3fc25b94ef96c305c874e477ae7e7aaeac7 100644 (file)
--- a/matita/matita/contribs/lambda/subterms/relocation.ma
+++ b/matita/matita/contribs/lambda/subterms/relocation.ma
@@ -41,8 +41,8 @@ lemma slift_id: ∀E,d. ↑[d, 0] E = E.
 ]
 qed.
 
-lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j.
-#b0 #j #d #Hjd #h * normalize
+lemma slift_inv_vref_lt: ∀c,j,d. j < d → ∀h,E. ↑[d, h] E = {c}#j → E = {c}#j.
+#c #j #d #Hjd #h * normalize
 [ #b #i elim (lt_or_eq_or_gt i d) #Hid
   [ >(tri_lt ???? … Hid) -Hid -Hjd //
   | #H destruct >tri_eq in Hjd; #H
@@ -56,9 +56,9 @@ lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E
 ]
 qed.
 
-lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
-                         d + h ≤ j ∧ E = {b0}#(j-h).
-#b0 #j #d #Hdj #h * normalize
+lemma slift_inv_vref_ge: ∀c,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {c}#j →
+                         d + h ≤ j ∧ E = {c}#(j-h).
+#c #j #d #Hdj #h * normalize
 [ #b #i elim (lt_or_eq_or_gt i d) #Hid
   [ >(tri_lt ???? … Hid) #H destruct
     lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
@@ -71,29 +71,29 @@ lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
 ]
 qed-.
 
-lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥.
-#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
+lemma slift_inv_vref_be: ∀c,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {c}#j → ⊥.
+#c #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
 lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
 elim (lt_refl_false … H)
 qed-.
 
-lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j →
-                              ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h).
-#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
+lemma slift_inv_vref_ge_plus: ∀c,j,d,h. d + h ≤ j →
+                              ∀E. ↑[d, h] E = {c}#j → E = {c}#(j-h).
+#c #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
 qed.
 
-lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U →
-                      ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T.
-#b0 #U #d #h * normalize
+lemma slift_inv_abst: ∀c,U,d,h,E. ↑[d, h] E = {c}𝛌.U →
+                      ∃∃T. ↑[d+1, h] T = U & E = {c}𝛌.T.
+#c #U #d #h * normalize
 [ #b #i #H destruct
 | #b #T #H destruct /2 width=3/
 | #b #V #T #H destruct
 ]
 qed-.
 
-lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
-                      ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
-#b0 #W #U #d #h * normalize
+lemma slift_inv_appl: ∀c,W,U,d,h,E. ↑[d, h] E = {c}@W.U →
+                      ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {c}@V.T.
+#c #W #U #d #h * normalize
 [ #b #i #H destruct
 | #b #T #H destruct
 | #b #V #T #H destruct /2 width=5/
@@ -240,13 +240,13 @@ qed-.
 lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) →
                        ∀l. sliftable (lstar S … R l).
 #S #R #HR #l #h #F1 #F2 #H
-@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/
 qed.
 
 lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
                             ∀l. sdeliftable_sn (lstar S … R l).
 #S #R #HR #l #h #G1 #G2 #H
-@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
+@(lstar_ind_l … l G1 H) -l -G1 /2 width=3/
 #a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
 elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
 elim (IHG2 … HFG) -G /3 width=3/