proposition: Lemma arbBool_correct: semProd arbitrary <--> [set: bool].
proof: Proof. rewrite /arbitrary /arbitrarySized /genBoolSized /=. rewrite semSized => n; split=> // _. exists n; split=> //. apply semElementsSize => //=; eauto with typeclass_instances. destruct n; repeat (try solve [left; auto]; right). Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)