X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind1%2Funwind_update.ma;h=69fcb47d5f9d44f8efebc5472cddf00d0803a710;hb=77479649510792efe4d9cbff508e118360862594;hp=9bdb32cdba72c91c173602d7c1c76edd0c48d30f;hpb=9b4e20442ec5a4028cfe2b6fe836c94acdb033b8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
index 9bdb32cdb..69fcb47d5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
@@ -23,7 +23,7 @@ include "ground/lib/stream_eq_eq.ma".
 
 lemma unwind_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
       ninj (m+⧣p+l) = ❘p❘ →
-      (▼[p]f1)@❨m❩ = (▼[p]f2)@❨m❩.
+      (▼[p]f1)＠⧣❨m❩ = (▼[p]f2)＠⧣❨m❩.
 #f1 #f2 #p @(list_ind_rcons … p) -p
 [ #m #l <depth_empty #H0 destruct
 | #p * [ #n ] #IH #m #l
@@ -43,7 +43,7 @@ lemma unwind_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
 qed.
 
 lemma unwind_rmap_pap_gt (f) (p) (m):
-      f@❨m+⧣p❩+❘p❘ = (▼[p]f)@❨m+❘p❘❩.
+      f＠⧣❨m+⧣p❩+❘p❘ = (▼[p]f)＠⧣❨m+❘p❘❩.
 #f #p @(list_ind_rcons … p) -p [ // ]
 #p * [ #n ] #IH #m
 [ <update_d_dx <depth_d_dx