// qed.
(* Basic inversions *********************************************************)
lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
// qed.
(* Basic inversions *********************************************************)
lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
#A * // #a #l >list_length_lcons #H
elim (eq_inv_nsucc_zero โฆ H)
qed-.
lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
#A * // #a #l >list_length_lcons #H
elim (eq_inv_nsucc_zero โฆ H)
qed-.
lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
/2 width=1 by list_length_inv_zero_dx/ qed-.
lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
/2 width=1 by list_length_inv_zero_dx/ qed-.
lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):