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=6490866044512e6f2b8587d171e2676e583953d7;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=72b4b347cec85096e2d2960bf72f40a3f309ab43;hpb=86861e6f031df66824a381527dfe847029ff72bc;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 72b4b347c..649086604 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
@@ -28,7 +28,7 @@ definition Omega3 (s): term ≝ +ⓓⓝ⋆s.(Delta s).(Omega1 s).
 
 (* Basic properties *********************************************************)
 
-lemma Delta_lifts (f) (s): ⬆*[f] (Delta s) ≘ (Delta s).
+lemma Delta_lifts (f) (s): ⇧*[f] (Delta s) ≘ (Delta s).
 /4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
 
 (* Basic inversion properties ***********************************************)