X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;h=efeaf86b40fb7087219bef1d55b705fd4c0c8ce0;hb=f83215ca9b8d0019c85a991ec90c6c658c0aaff8;hp=e76c4943b704ce2729085a27fe150c8decb87448;hpb=e8571cfbc30a3da656cff0c0e0f0ee747e8c4cdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index e76c4943b..efeaf86b4 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -39,7 +39,7 @@ interpretation
 lemma depth_empty: 𝟎 = ❘𝐞❘.
 // qed.
 
-lemma depth_d (q) (n): ❘q❘ = ❘𝗱❨n❩◗q❘.
+lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
 // qed.
 
 lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.