update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / lenv_length.ma

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 8b7ccd58207a7b1fc92fc4203da6f70612a7982c..d2690db960f24ca0950f85668e56106ff582e1f7 100644 (file)
--- 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.