proposition: Lemma semBindOptSizeOpt_subset_compat (A B : Type) (g g' : G (option A)) (f f' : A -> G (option B)) s : semProdSizeOpt g s \subset semProdSizeOpt g' s -> (forall (x : A), semProdSizeOpt (f x) s \subset semProdSizeOpt (f' x) s) -> semProdSizeOpt (bindOpt g f) s \subset semProdSizeOpt (bindOpt g' f') s.
proof: Proof. intros Hyp1 Hyp2. rewrite !semOptBindOptSize. eapply incl_bigcup_compat; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)