proposition: Lemma monad_leftid : forall {A B : Type} (a: A) (f : A -> G B), semProd (bind (ret a) f) <--> semProd (f a).
proof: Proof. intros. rewrite /semProd. apply eq_bigcupr => size. rewrite semBindSize semReturnSize bigcup_set1. reflexivity. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)