(* 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 (â\92º) (â\92º)
| 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)"