proposition: Lemma internalize_pure {a b c} (f : Kleisli (stateT S M) a b) (g : S * b -> S * c) : internalize f >>> pure g ⩯ (internalize (f >>> (fun b s => ret (g (s,b))))).
proof: Proof. repeat red. destruct a0. unfold internalize, cat, Cat_Kleisli. cbn. apply Proper_bind; auto. - reflexivity. - repeat red. destruct a1. unfold pure. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Monad)