proposition: Lemma internalize_eq {a b:Type} (f g : Kleisli (stateT S M) a b) : eq2 f g <-> eq2 (internalize f) (internalize g).
proof: Proof. split. - intros. repeat red. destruct a0. unfold internalize. cbn. apply H. - intros. repeat red. intros. unfold internalize in H. specialize (H (a1, a0)). apply H. Qed.
imports: Coq(Setoid Morphisms) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Monad)