X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv_length.ma;h=a7a99ba015b8ed5fcaec9c8fa7a1d41af3ca0510;hb=ebc170efe71cf4ee842acfbe58bb6864e76ba98c;hp=f608f8c3c26189e7910c2f36ce4257c4f29239c8;hpb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
index f608f8c3c..a7a99ba01 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
@@ -41,16 +41,18 @@ qed-.
 lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
 /2 width=1 by length_inv_zero_dx/ qed-.
 
-lemma length_inv_pos_dx: ∀n,L. |L| = ⫯n →
-                         ∃∃I,K,V. |K| = n & L = K. ⓑ{I}V.
+(* Basic_2A1: was: length_inv_pos_dx *)
+lemma length_inv_succ_dx: ∀n,L. |L| = ⫯n →
+                          ∃∃I,K,V. |K| = n & L = K. ⓑ{I}V.
 #n * /3 width=5 by injective_S, ex2_3_intro/
 >length_atom #H destruct
 qed-.
 
-lemma length_inv_pos_sn: ∀n,L. ⫯n = |L| →
-                         ∃∃I,K,V. n = |K| & L = K. ⓑ{I}V.
+(* Basic_2A1: was: length_inv_pos_sn *)
+lemma length_inv_succ_sn: ∀n,L. ⫯n = |L| →
+                          ∃∃I,K,V. n = |K| & L = K. ⓑ{I}V.
 #l #L #H lapply (sym_eq ??? H) -H 
-#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/
+#H elim (length_inv_succ_dx … H) -H /2 width=5 by ex2_3_intro/
 qed-.
 
 (* Basic_2A1: removed theorems 1: length_inj *)