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