X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Flenv_length.ma;h=d2690db960f24ca0950f85668e56106ff582e1f7;hb=26d2ecb945a881c61d03f3c259996374209f5d7f;hp=8b7ccd58207a7b1fc92fc4203da6f70612a7982c;hpb=1c8e230b1d81491b38126900d76201fb84303ced;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma
index 8b7ccd582..d2690db96 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma
@@ -23,8 +23,6 @@ rec definition length L ≝ match L with
 
 interpretation "length (local environment)" 'card L = (length L).
 
-definition length2 (L1) (L2): nat ≝ |L1| + |L2|. 
-
 (* Basic properties *********************************************************)
 
 lemma length_atom: |⋆| = 0.