proposition: Lemma right_module_law2 {A} : α ∙ fmap F (μ A) ∼ α ∙ α.
proof: Proof. cbv. rewrite -(rm_law3 rmF) cat_law1 rm_law2_id; reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)