proposition: Fact cat_pure {A B C}: forall (ab: Kleisli m A B) (g:B -> C), (ab >>> pure g) ⩯ (map g ab).
proof: Proof. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)