+(* Basic_2A1: includes: liftv_total *)
+lemma liftsv_total: ∀f. ∀T1s:list term. ∃T2s. ⬆*[f] T1s ≡ T2s.
+#f #T1s elim T1s -T1s
+[ /2 width=2 by liftsv_nil, ex_intro/
+| #T1 #T1s * #T2s #HT12s
+ elim (lifts_total T1 f) /3 width=2 by liftsv_cons, ex_intro/
+]
+qed-.
+