proposition: Lemma sum_enum_ok (X: finType) (Y: finType) x : count (toSumList1 Y (elem X) ++ toSumList2 X (elem Y)) x = 1.
proof: Proof. rewrite <- countSplit. apply proveOne. destruct x. - left. split; cbn. + rewrite toSumList1_count. apply enum_ok. + apply toSumList2_missing. - right. split; cbn. + rewrite toSumList2_count. apply enum_ok. + apply toSumList1_missing. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypes)