(* GENERIC TERM VECTOR RELOCATION *******************************************)
inductive liftsv (cs:mr2) : relation (list term) ≝
-| liftsv_nil : liftsv cs (â\92º) (â\92º)
+| 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)