proposition: Lemma translate_iter {E F I R} (b: I -> itree E (I + R)) (h: E ~> F) i: translate h (ITree.iter b i) ≈ ITree.iter (fun x => translate h (b x)) i.
proof: Proof. rewrite translate_to_interp. rewrite interp_iter'_eutt. reflexivity. clear i. intros i. cbn. rewrite translate_to_interp. 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)