X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fvoids_length.ma;h=c280cee4ebf6c51650bbc6a891c7a000357b980a;hb=1c8e230b1d81491b38126900d76201fb84303ced;hp=510a05f681ad39fddbccb2a69f165bad68914d3c;hpb=dc9c7181b2dc66c8d297f708324dcdeea98bc4d8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma
index 510a05f68..c280cee4e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma
@@ -24,6 +24,9 @@ lemma length_void: ∀L,n. n+|L| = |ⓧ*[n]L|.
 #n #IH <voids_succ >length_bind <IH -IH //
 qed.
 
+lemma length_void_le: ∀L,n. |L| ≤ |ⓧ*[n]L|.
+// qed.
+
 (* Main forward properties with length for local environments ***************)
 
 theorem voids_inj_length: ∀n1,n2,L1,L2. ⓧ*[n1]L1 = ⓧ*[n2]L2 →