proposition: Lemma interp_loop {E F} (f : E ~> itree F) {A B C} (t : C + A -> itree E (C + B)) a : interp f (loop (C := ktree E) t a) ≅ loop (C := ktree F) (fun ca => interp f (t ca)) a.
proof: Proof. unfold loop. unfold cat, Cat_Kleisli, ITree.cat; cbn. rewrite interp_bind. apply eqit_bind. { unfold inr_, Inr_Kleisli, lift_ktree, pure; cbn. rewrite interp_ret. reflexivity. } repeat intro. rewrite interp_iter. apply eq_itree_iter. intros ? ? []. rewrite interp_bind. apply eqit_bind; try reflexivity. intros []; cbn. unfold cat. rewrite interp_bind. - unfold inl_, Inl_Kleisli, inr_, Inr_Kleisli, lift_ktree; cbn. rewrite interp_ret, !bind_ret_l, interp_ret. reflexivity. - unfold cat, id_, Id_Kleisli, inr_, Inr_Kleisli, lift_ktree, pure; cbn. rewrite interp_bind, interp_ret, !bind_ret_l, interp_ret. 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)