proposition: Lemma joinMret : JoinLaws.right_unit ret join.
proof: Proof. rewrite /join => A; rewrite funeqE => ma. rewrite bind_fmap_fun/= -[in RHS](bindmret ma). congr (fun f => bind f ma). by rewrite hom_ext. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)