∃∃T1,T1s. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1s ≡ T2s &
X = T1 @ T1s.
/2 width=3 by liftsv_inv_cons2_aux/ qed-.
(* Basic_1: was: lifts1_flat (left to right) *)
∃∃T1,T1s. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1s ≡ T2s &
X = T1 @ T1s.
/2 width=3 by liftsv_inv_cons2_aux/ qed-.
(* Basic_1: was: lifts1_flat (left to right) *)