(* Basic properties *********************************************************)
-lemma Delta_lifts (f) (s): â¬\86*[f] (Delta s) ≘ (Delta s).
+lemma Delta_lifts (f) (s): â\87§*[f] (Delta s) ≘ (Delta s).
/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
(* Basic inversion properties ***********************************************)