/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].
#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 →
∃∃I,K. |K| = n & L = K. ⓘ[I].
#n *