\lambda\delta web site update for git

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

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 510a05f681ad39fddbccb2a69f165bad68914d3c..c280cee4ebf6c51650bbc6a891c7a000357b980a 100644 (file)
--- 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 →