(* GENERIC TERM VECTOR RELOCATION *******************************************)
-inductive liftsv (cs:list2 nat nat) : relation (list term) ≝
+inductive liftsv (cs:list2 ynat nat) : relation (list term) ≝
| liftsv_nil : liftsv cs (◊) (◊)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →