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 88952c2bc0b4b4edcd60a53c291f1c85a7a4866c..1634678af36ecc77d57b90df7e0b6dddeb4fbab0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,13 +13,14 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
+include "ground/arith/nat_succ.ma".
 include "ground/notation/functions/verticalbars_1.ma".
 
 (* DEPTH FOR PATH ***********************************************************)
 
-rec definition depth (p) on p: pnat ≝
+rec definition depth (p) on p: nat ≝
 match p with
-[ list_empty     â\87\92 ð\9d\9f\8f
+[ list_empty     â\87\92 ð\9d\9f\8e
 | list_lcons l q ⇒
   match l with
   [ label_d _ ⇒ depth q
@@ -36,7 +37,7 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: ð\9d\9f\8f = ❘𝐞❘.
+lemma depth_empty: ð\9d\9f\8e = ❘𝐞❘.
 // qed.
 
 lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.