proposition: Lemma toSumList1_count (X: eqType) (x: X) (Y: eqType) (A: list X) : count (toSumList1 Y A) (inl x) = count A x .
proof: Proof. induction A; simpl; dec; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypes)