proposition: Lemma semLiftProdSize {A B} (f: A -> B) (g: G A) size : semProdSize (liftM f g) size <--> f @: (semProdSize g size).
proof: Proof. by rewrite semBindSize (eq_bigcupr _ (fun a => semReturnSize (f a) size)). Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)