proposition: Lemma translate_to_interp {E F R} (f : E ~> F) (t : itree E R) : translate f t ≈ interp (fun _ e => ITree.trigger (f _ e)) t.
proof: Proof. revert t. einit. ecofix CIH. intros. rewrite unfold_translate. rewrite unfold_interp. destruct (observe t); try estep. unfold ITree.trigger. simpl. rewrite bind_vis. evis. intros. rewrite bind_ret_l, tau_euttge. auto with paco. 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)