X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Farith_2a.ma;h=a136174bc8b209fc0c813c013b3382cdca587938;hp=92224c4c9560d1f51b5c54e52c144fda38b2ec00;hb=48cd63fc7f4415925582eae224a36a9c1bb3cc06;hpb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
index 92224c4c9..a136174bc 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
@@ -12,16 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/two_0.ma".
+include "ground/arith/pnat_two.ma".
 include "ground/arith/nat_le_minus_plus.ma".
 include "ground/arith/nat_lt.ma".
 
 (* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************)
 
-interpretation
-  "zero (non-negative integers)"
-  'Two = (ninj (psucc punit)).
-
 (* Equalities ***************************************************************)
 
 lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.