proposition: Fact compose_pure_r {A B C D} (f: B -> C) (g: C -> D) (k: Kleisli m A B) : ((k >>> pure f) >>> pure g ⩯ k >>> pure (g ∘ f))%cat.
proof: Proof. rewrite cat_assoc. rewrite compose_pure. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)