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