proposition: Lemma eutt_eq_interp_state_iter {E F S} (f: E ~> stateT S (itree F)) {I A} (t : I -> itree E (I + A)): forall i s, interp_state f (ITree.iter t i) s ≈ Basics.iter (fun i => interp_state f (t i)) i s.
proof: Proof. unfold Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree in *; cbn. ginit. gcofix CIH; intros i s. rewrite 2 unfold_iter; cbn. rewrite !bind_bind. setoid_rewrite bind_ret_l. rewrite interp_state_bind. guclo eqit_clo_bind; econstructor; eauto. reflexivity. intros [s' []] _ []; cbn. - rewrite interp_state_tau. gstep; constructor. auto with paco. - rewrite interp_state_ret; apply 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)