proposition: Lemma eq2_to_eq1 : forall a b (f g : Kleisli (stateT S M) a b) (x:a) (s:S), eq2 f g -> eq1 (f x s) (g x s).
proof: Proof. intros a b f g x s H. apply H. Qed.
imports: Coq(Setoid Morphisms) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Monad)