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=30738ee24709f3b42e7ddb6d41bf41de4c0b1e42;hpb=b40ccca541b378319b076b1bb36c435dfdf2a55f;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 30738ee24..c280cee4e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma
@@ -15,14 +15,17 @@
 include "basic_2/syntax/lenv_length.ma".
 include "basic_2/syntax/voids.ma".
 
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
+(* EXTENSION OF A LOCAL ENVIRONMENT WITH EXCLUSION BINDERS ******************)
 
-(* Forward lemmas with length for local environments ************************)
+(* Properties with length for local environments ****************************)
 
-lemma voids_fwd_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
-                        |L1| + n2 = |L2| + n1.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize //
-#I1 #I2 #K1 #K2 #V #n #_ #IH 
+lemma length_void: ∀L,n. n+|L| = |ⓧ*[n]L|.
+#L #n elim n -n //
+#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 ***************)