proposition: Lemma monad_rightid : forall {A : Type} (g : G A), semProd (bind g ret) <--> semProd g.
proof: Proof. intros; rewrite /semProd. apply: eq_bigcupr => size; rewrite semBindSize. rewrite (eq_bigcupr _ (fun x => semReturnSize x size)). apply coverE. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)