proposition: Lemma internalize_cat {a b c} (f : Kleisli (stateT S M) a b) (g : Kleisli (stateT S M) b c) : (internalize (f >>> g)) ⩯ ((internalize f) >>> (internalize g)).
proof: Proof. repeat red. destruct a0. cbn. unfold internalize. unfold cat, Cat_Kleisli. cbn. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Monad)