proposition: Lemma join_right_unit : JoinLaws.right_unit ret join.
proof: Proof. move=> a; rewrite joinE. rewrite /M FCompE. rewrite /= -functor_o -[in RHS]functor_id. congr (G # _). by rewrite hom_ext/= triL. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)