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

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 d2690db96..8b7ccd582 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma
@@ -23,6 +23,8 @@ 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.