proposition: Lemma monad_assoc A B C (ga : G A) (fb : A -> G B) (fc : B -> G C) : semProd (bind (bind ga fb) fc) <--> semProd (bind ga (fun a => bind (fb a) fc)).
proof: Proof. apply eq_bigcupr => ?; rewrite !semBindSize ?bigcup_flatten. by apply eq_bigcupr => ?; rewrite !semBindSize ?bigcup_flatten. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)