proposition: Lemma semLiftGen {A B} (f: A -> B) (g: G A) : semProd (liftM f g) <--> f @: semProd g.
proof: Proof. rewrite imset_bigcup. apply: eq_bigcupr => size. 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)