proposition: Lemma interp_iter'_eutt {E F} (f: E ~> itree F) {I A} (t : I -> itree E (I + A)) (t': I -> itree F (I + A)) (Heq: forall i, interp f (t i) ≈ t' i): forall i, interp f (ITree.iter t i) ≈ ITree.iter t' i.
proof: Proof. ginit. gcofix CIH; intros i. rewrite 2 unfold_iter. rewrite interp_bind. guclo eqit_clo_bind; econstructor; eauto. apply Heq. intros [] _ []; cbn. - rewrite interp_tau; gstep; constructor; auto with paco. - rewrite interp_ret. gstep; constructor; auto. 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)