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