update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / examples / ex_cpr_omega.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
index 0bbe88b883b69ac1f7a4b6b73bacbf4bdbe92fd4..7ebb0a3455b51a3ca5042c8a035c379df1638f34 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
@@ -26,8 +26,8 @@ definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0.
 
 (* 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 **********************************************************)