proposition: Lemma interp_state_vis {E F : Type -> Type} {S T U : Type} (e : E T) (k : T -> itree E U) (h : E ~> Monads.stateT S (itree F)) (s : S) : interp_state h (Vis e k) s ≅ h T e s >>= fun sx => Tau (interp_state h (k (snd sx)) (fst sx)).
proof: Proof. rewrite unfold_interp_state; 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)