(* Basic properties *********************************************************)
-lemma Delta_lifts: â\88\80W1,W2,f. â¬\86*[f] W1 â\89¡ W2 →
- â¬\86*[f] (Delta W1) â\89¡ (Delta W2).
+lemma Delta_lifts: â\88\80W1,W2,f. â¬\86*[f] W1 â\89\98 W2 →
+ â¬\86*[f] (Delta W1) â\89\98 (Delta W2).
/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
(* Main properties **********************************************************)