proposition: Fact pure_cat {A B C}: forall (f:A -> B) (bc: Kleisli m B C), pure f >>> bc ⩯ fun a => bc (f a).
proof: Proof. intros; intro a. unfold pure, pure, cat, Cat_Kleisli. rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)