proposition: Lemma semBindSize_subset_compat {A B : Type} (g g' : G A) (f f' : A -> G B) : (forall s, semProdSize g s \subset semProdSize g' s) -> (forall x s, semProdSize (f x) s \subset semProdSize (f' x) s) -> (forall s, semProdSize (bind g f) s \subset semProdSize (bind g' f') s).
proof: Proof. intros Hs1 Hs2 s. rewrite !semBindSize. specialize (Hs1 s). eapply incl_bigcup_compat; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)