-inductive liftsv (t:trace) : relation (list term) ≝
-| liftsv_nil : liftsv t (◊) (◊)
-| liftsv_cons: ∀T1s,T2s,T1,T2.
- ⬆*[t] T1 ≡ T2 → liftsv t T1s T2s →
- liftsv t (T1 @ T1s) (T2 @ T2s)
+inductive liftsv (f): relation (list term) ≝
+| liftsv_nil : liftsv f (◊) (◊)
+| liftsv_cons: ∀T1c,T2c,T1,T2.
+ ⬆*[f] T1 ≡ T2 → liftsv f T1c T2c →
+ liftsv f (T1 @ T1c) (T2 @ T2c)