X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Flenv_length.ma;h=164aab50091367330f04be1f04453f3c29f16e62;hb=8d8863982ca95225551e9659ed431db046c34e81;hp=52dfc3516e8b355a9b86a70543b3c462a606f2c6;hpb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma
index 52dfc3516..164aab500 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma
@@ -12,12 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/arith/nat_succ.ma".
 include "static_2/syntax/lenv.ma".
 
 (* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
 
 rec definition length L ≝ match L with
-[ LAtom     ⇒ 0
+[ LAtom     ⇒ 𝟎
 | LBind L _ ⇒ ↑(length L)
 ].
 
@@ -25,36 +26,39 @@ interpretation "length (local environment)" 'card L = (length L).
 
 (* Basic properties *********************************************************)
 
-lemma length_atom: |⋆| = 0.
+lemma length_atom: |⋆| = 𝟎.
 // qed.
 
 (* Basic_2A1: uses: length_pair *)
-lemma length_bind: ∀I,L. |L.ⓘ{I}| = ↑|L|.
+lemma length_bind: ∀I,L. |L.ⓘ[I]| = ↑|L|.
 // qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
-* // #L #I >length_bind
-#H destruct
+lemma length_inv_zero_dx: ∀L. |L| = 𝟎 → L = ⋆.
+* // #L #I
+>length_bind #H
+elim (eq_inv_nsucc_zero … H) 
 qed-.
 
-lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
+lemma length_inv_zero_sn: ∀L. 𝟎 = |L| → L = ⋆.
 /2 width=1 by length_inv_zero_dx/ qed-.
 
 (* Basic_2A1: was: length_inv_pos_dx *)
 lemma length_inv_succ_dx: ∀n,L. |L| = ↑n →
-                          ∃∃I,K. |K| = n & L = K. ⓘ{I}.
+                          ∃∃I,K. |K| = n & L = K. ⓘ[I].
 #n *
-[ >length_atom #H destruct
-| #L #I >length_bind /3 width=4 by ex2_2_intro, injective_S/
+[ >length_atom #H
+  elim (eq_inv_zero_nsucc … H) 
+| #L #I >length_bind
+  /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/
 ]
 qed-.
 
 (* Basic_2A1: was: length_inv_pos_sn *)
 lemma length_inv_succ_sn: ∀n,L. ↑n = |L| →
-                          ∃∃I,K. n = |K| & L = K. ⓘ{I}.
-#n #L #H lapply (sym_eq ??? H) -H 
+                          ∃∃I,K. n = |K| & L = K. ⓘ[I].
+#n #L #H lapply (sym_eq ??? H) -H
 #H elim (length_inv_succ_dx … H) -H /2 width=4 by ex2_2_intro/
 qed-.