/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
(* Basic inversion properties ***********************************************)
/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
(* Basic inversion properties ***********************************************)