proposition: Lemma NoneElement (X: eqType) (A: list X) : count (toOptionList A) None = 1.
proof: Proof. unfold toOptionList. simpl. dec; try congruence. f_equal. induction A. - reflexivity. - simpl; dec; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypes)