proposition: Lemma arbBool_correctSize s : semProdSize arbitrary s <--> [set: bool].
proof: Proof. rewrite /arbitrary //=. rewrite semSizedSize semElementsSize //; split=> /RandomQC.leq _ //=; case a=> //=. repeat (try solve [left; auto]; right). 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)