X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fexamples%2Fex_cpr_omega.ma;h=7ebb0a3455b51a3ca5042c8a035c379df1638f34;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=0bbe88b883b69ac1f7a4b6b73bacbf4bdbe92fd4;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

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 0bbe88b88..7ebb0a345 100644
--- 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: ∀W1,W2,f. ⬆*[f] W1 ≡ W2 →
-                   ⬆*[f] (Delta W1) ≡ (Delta W2).
+lemma Delta_lifts: ∀W1,W2,f. ⬆*[f] W1 ≘ W2 →
+                   ⬆*[f] (Delta W1) ≘ (Delta W2).
 /4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
 
 (* Main properties **********************************************************)