proposition: Lemma semOptBindOptSize A B (g : G (option A)) (f : A -> G (option B)) size : semProdSizeOpt (bindOpt g f) size <--> \bigcup_(a in semProdSizeOpt g size) semProdSizeOpt (f a) size.
proof: Proof. unfold bindOpt. rewrite semOptBindSize; eauto. - split. + intros Hin. inv Hin. inv H. destruct x. eexists. split; eauto. eapply semReturnSizeOpt_None in H1. inv H1. + 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)