proposition: Lemma unfold_interp {E F R} {f : E ~> itree F} (t : itree E R) : interp f t ≅ (_interp f (observe t)).
proof: Proof. unfold interp, Basics.iter, MonadIter_itree. rewrite unfold_iter. destruct (observe t); cbn; rewrite ?bind_ret_l, ?bind_map. all: try reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp Interp.Handler Interp.TranslateFacts)