| liftsv_nil : liftsv f (Ⓔ) (Ⓔ)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⇧*[f] T1 ≘ T2 → liftsv f T1s T2s →
liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
.
| liftsv_nil : liftsv f (Ⓔ) (Ⓔ)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⇧*[f] T1 ≘ T2 → liftsv f T1s T2s →
liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
.