qed-.
(* Basic_2A1: was: length_inv_pos_sn_ltail *)
lemma length_inv_succ_sn_ltail: ∀L,n. ↑n = |L| →
∃∃I,K. n = |K| & L = ⓘ[I].K.
#Y #n #H elim (length_inv_succ_sn … H) -H #I #L #Hn #HLK destruct
qed-.
(* Basic_2A1: was: length_inv_pos_sn_ltail *)
lemma length_inv_succ_sn_ltail: ∀L,n. ↑n = |L| →
∃∃I,K. n = |K| & L = ⓘ[I].K.
#Y #n #H elim (length_inv_succ_sn … H) -H #I #L #Hn #HLK destruct