proposition: Lemma interp_state_tau {E F : Type -> Type} S {T : Type} (t : itree E T) (h : E ~> Monads.stateT S (itree F)) (s : S) : interp_state h (Tau t) s ≅ Tau (interp_state h t s).
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)