proposition: Lemma rm_law2_id {A B} (g : C⦅A ; M B⦆) : rm_bind rmF (relmon_bind M g) ∼ rm_bind rmF g ∙ rm_bind rmF (Id (M A)).
proof: Proof. rewrite -(cat_law2 _ _ _ (relmon_bind M g)) rm_law2 ; reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)