proposition: Lemma semLiftProd2Size {A1 A2 B} (f: A1 -> A2 -> B) (g1 : G A1) (g2 : G A2) s : semProdSize (liftM2 f g1 g2) s <--> f @2: (semProdSize g1 s, semProdSize g2 s).
proof: Proof. rewrite semBindSize curry_imset2l; apply: eq_bigcupr => x. by rewrite semBindSize; apply: eq_bigcupr => y; rewrite semReturnSize. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)