proposition: Lemma SomeElement (X: eqType) (A: list X) x: count (toOptionList A) (Some x) = count A x .
proof: Proof. unfold toOptionList. simpl. dec; try congruence. induction A. + tauto. + simpl. dec; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypes)