partial update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / genv_length.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma
index afd36af9c34496f225ce0b042f9c06117b655e1d..41e22b52c728754f171eff185715c212660612b6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma
@@ -12,12 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/arith/nat_succ.ma".
 include "static_2/syntax/genv.ma".
 
 (* LENGTH OF A GLOBAL ENVIRONMENT *******************************************)
 
 rec definition glength G on G ≝ match G with
-[ GAtom       ⇒ 0
+[ GAtom       ⇒ 𝟎
 | GPair G _ _ ⇒ ↑(glength G)
 ].