X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fgenv_length.ma;h=41e22b52c728754f171eff185715c212660612b6;hp=afd36af9c34496f225ce0b042f9c06117b655e1d;hb=156d974ad89aa04a086fdf9d332c8b04adf279fd;hpb=8fe4dc148d50a0352313633bea61441bc817afbf

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 afd36af9c..41e22b52c 100644
--- 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)
 ].