proposition: Lemma rmon_id_law1 {A} : μ ∙ (fmap M η) ∼ Id (M A).
proof: Proof. cbv. rewrite -relmon_law3 cat_law3 (relmon_law2 M0) cat_law1 relmon_law1. reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)