#A * /2 width=4 by ex2_2_intro/
>length_nil #x #H destruct
qed-.
lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| →
#A * /2 width=4 by ex2_2_intro/
>length_nil #x #H destruct
qed-.
lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| →