X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fexamples%2Fex_cpr_omega.ma;h=ef27dfa48f0c2e7bc223a56ec6b251c59ff58459;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=6a2586ff16fb2d24d2f8769b645e1cccb586b4e1;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
index 6a2586ff1..ef27dfa48 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
@@ -26,8 +26,8 @@ definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0.
 
 (* Basic properties *********************************************************)
 
-lemma Delta_lift: ∀W1,W2,d,e. ⇧[d, e] W1 ≡ W2 →
-                  ⇧[d, e] (Delta W1) ≡ (Delta W2).
+lemma Delta_lift: ∀W1,W2,d,e. ⬆[d, e] W1 ≡ W2 →
+                  ⬆[d, e] (Delta W1) ≡ (Delta W2).
 /4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
 
 (* Main properties **********************************************************)