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

[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 30738ee24709f3b42e7ddb6d41bf41de4c0b1e42..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
@@ -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 ***************)