update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind1 / unwind_structure_depth.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
index c13471e810765e89fa3ff41384172ff8da11fd30..df3423e164aa3107f8d5c2407ccc6581b315e20b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
@@ -22,7 +22,7 @@ include "ground/arith/nat_pred_succ.ma".
 (* Basic constructions with structure and depth ****************************)
 
 lemma unwind_rmap_structure (p) (f):
-      (⫯*[â\9d\98pâ\9d\98]f) = ▼[⊗p]f.
+      (⫯*[â\99­p]f) = ▼[⊗p]f.
 #p elim p -p //
 * [ #n ] #p #IH #f //
 [ <unwind_rmap_A_sn //