include "static_2/syntax/lenv.ma".
(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
rec definition length L ≝ match L with
include "static_2/syntax/lenv.ma".
(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
rec definition length L ≝ match L with
/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 →
/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 →
-[ >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| →
]
qed-.
(* Basic_2A1: was: length_inv_pos_sn *)
lemma length_inv_succ_sn: ∀n,L. ↑n = |L| →