proposition: Lemma interp_state_ret {E F : Type -> Type} {R S : Type} (f : forall T, E T -> S -> itree F (S * T)%type) (s : S) (r : R) : (interp_state f (Ret r) s) ≅ (Ret (s, r)).
proof: Proof. rewrite itree_eta. reflexivity. Qed.
imports: Coq(Program.Tactics Morphisms) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts Events.State)