proposition: Lemma prod_enum_ok (T1 T2: finType) (x: T1 * T2): count (list_prod (elem T1) (elem T2)) x = 1.
proof: Proof. destruct x as [x y]. rewrite ProdCount. unfold elem. now repeat rewrite enum_ok. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypes)