proposition: Lemma interp_state_iter' {E F } S (f : E ~> stateT S (itree F)) {I A} (t : I -> itree E (I + A)) : forall i, state_eq (State.interp_state f (ITree.iter t i)) (Basics.iter (fun i => State.interp_state f (t i)) i).
proof: Proof. eapply interp_state_iter. intros i. red. 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)