work in progress with voids and lveq (was: the most recent voids)

[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 d2690db960f24ca0950f85668e56106ff582e1f7..8b7ccd58207a7b1fc92fc4203da6f70612a7982c 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,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.