(* GENERIC TERM VECTOR RELOCATION *******************************************)
-inductive liftsv (cs:list2 nat nat) : relation (list term) ≝
-| liftsv_nil : liftsv cs (â\97\8a) (â\97\8a)
+inductive liftsv (cs:mr2) : relation (list term) ≝
+| liftsv_nil : liftsv cs (â\93\94) (â\93\94)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →
- liftsv cs (T1 @ T1s) (T2 @ T2s)
+ liftsv cs (T1 ⨮ T1s) (T2 ⨮ T2s)
.
interpretation "generic relocation (vector)"
(* Basic inversion lemmas ***************************************************)
-(* Basic_1: was: lifts1_flat (left to right) *)
lemma lifts_inv_applv1: ∀V1s,U1,T2,cs. ⬆*[cs] Ⓐ V1s. U1 ≡ T2 →
∃∃V2s,U2. ⬆*[cs] V1s ≡ V2s & ⬆*[cs] U1 ≡ U2 &
T2 = Ⓐ V2s. U2.
(* Basic properties *********************************************************)
-(* Basic_1: was: lifts1_flat (right to left) *)
lemma lifts_applv: ∀V1s,V2s,cs. ⬆*[cs] V1s ≡ V2s →
∀T1,T2. ⬆*[cs] T1 ≡ T2 →
⬆*[cs] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.