proposition: Lemma unfold_interp_state {E F S R} (h : E ~> Monads.stateT S (itree F)) (t : itree E R) s : eq_itree eq (interp_state h t s) (_interp_state h (observe t) s).
proof: Proof. unfold interp_state, interp, Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree; cbn. rewrite unfold_iter; cbn. destruct observe; cbn. - rewrite 2 bind_ret_l. reflexivity. - rewrite 2 bind_ret_l. reflexivity. - rewrite bind_map, bind_bind; cbn. setoid_rewrite bind_ret_l. apply eqit_bind; 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)