update in ground

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

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 ed025110a54db56bbb60b7f7b96d59fc0ba0d6d7..0f52a185889d91d3a8955f4df7e920d36d09f522 100644 (file)
--- 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