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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
index ed025110a..0f52a1858 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
@@ -74,7 +74,7 @@ qed-.
 (* Advanced constructions with proj_path ************************************)
 
 lemma unwind_path_d_empty_dx (n) (p) (f):
-      (âp)âð±((â¼[p]f)@â¨nâ©) = â¼[f](pâð±n).
+      (âp)âð±((â¼[p]f)ï¼ â§£â¨nâ©) = â¼[f](pâð±n).
 #n #p #f <unwind_append_proper_dx // 
 qed.
 
@@ -110,7 +110,7 @@ qed-.
 
 lemma unwind_path_inv_d_sn (k) (q) (p) (f):
       (ð±kâq) = â¼[f]p â
-      ââr,h. ð = âr & (â¼[r]f)@â¨hâ© = k & ð = q & râð±h = p.
+      ââr,h. ð = âr & (â¼[r]f)ï¼ â§£â¨hâ© = k & ð = q & râð±h = p.
 #k #q #p @(path_ind_unwind â¦ p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct