update in delayed updating

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

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 e76c4943b704ce2729085a27fe150c8decb87448..efeaf86b40fb7087219bef1d55b705fd4c0c8ce0 100644 (file)
--- 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❘.