proposition: Lemma semOptBindSize A B (g : G A) (f : A -> G (option B)) size : semProdSizeOpt (bind g f) size <--> \bigcup_(a in semProdSize g size) semProdSizeOpt (f a) size.
proof: Proof. unfold semProdSizeOpt. rewrite semBindSize; eauto. split. - intros Hin. inv Hin. inv H. eexists. split; eauto. - intros Hin. inv Hin. inv H. eexists. split; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)