- ng_kernel: we print the offending term when guarded_by_constructors fails

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / lenv_length.ma

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 f608f8c3c26189e7910c2f36ce4257c4f29239c8..a7a99ba015b8ed5fcaec9c8fa7a1d41af3ca0510 100644 (file)
--- 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 *)