proposition: Lemma arbList_correct: forall {A} `{H : Arbitrary A} (P : nat -> A -> Prop) s, (semProdSize arbitrary s <--> P s) -> (semProdSize arbitrary s <--> (fun (l : list A) => length l <= s /\ (forall x, List.In x l -> P s x))).
proof: Proof. move => A G S H P s Hgen l. rewrite !/arbitrary /genList. split. - move => /semListOfSize [Hl Hsize]. split => // x HIn //=. apply Hgen. auto. - move => [Hl HP]. apply semListOfSize; eauto with typeclass_instances. split => // x HIn. apply Hgen. auto. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)