update in delayed updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_structure.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 6ba6e937b48778b995bae2d16e1ca16f326ce13f..8c60eea7595c8a88c43250865500b11010701dee 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -40,7 +40,7 @@ lemma structure_empty:
 // qed.
 
 lemma structure_d_sn (p) (n):
-      ⊗p = ⊗(𝗱❨n❩◗p).
+      ⊗p = ⊗(𝗱n◗p).
 // qed.
 
 lemma structure_L_sn (p):
@@ -71,7 +71,7 @@ qed.
 (* Constructions with list_rcons ********************************************)
 
 lemma structure_d_dx (p) (n):
-      ⊗p = ⊗(p◖𝗱❨n❩).
+      ⊗p = ⊗(p◖𝗱n).
 #p #n <structure_append //
 qed.