include "basic_2/notation/relations/rat_3.ma".
include "basic_2/grammar/term_vector.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
include "basic_2/notation/relations/rat_3.ma".
include "basic_2/grammar/term_vector.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-| at_lt : ∀cs,l,m,i1,i2. i1 < l →
+| at_lt : ∀cs,l,m,i1,i2. yinj i1 < l →
-| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
+| at_ge : ∀cs,l,m,i1,i2. l ≤ yinj i1 →
qed-.
lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
qed-.
lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1