proposition: Lemma arbPair_correctSize {A B} `{Arbitrary A} `{Arbitrary B} (Sa : nat -> set A) (Sb : nat -> set B) s: (semProdSize arbitrary s <--> Sa s) -> (semProdSize arbitrary s <--> Sb s) -> (semProdSize arbitrary s <--> setX (Sa s) (Sb s)).
proof: Proof. move => Hyp1 Hyp2 . Opaque liftM2. simpl. rewrite semLiftProd2Size; move => [a b]. split. by move => [[a' b'] [[/= /Hyp1 Ha /Hyp2 Hb] [Heq1 Heq2]]]; subst; split. move => [/Hyp1 Ha /Hyp2 Hb]. eexists; split; first by split; eauto. reflexivity. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)