proposition: Lemma cat_iter: forall {E: Type -> Type} {a b c} (f: ktree E a (a + b)) (g: ktree E b (b + c)), ITree.iter f >>> ITree.iter g ⩯ inl_ >>> ITree.iter (case_ (f >>> inl_) (g >>> inr_ >>> assoc_l)).
proof: Proof. intros *. unfold_ktree. einit. intros. revert a0. ecofix CIH. intros. cbn. rewrite bind_ret_l. match goal with |- euttG _ _ _ _ _ ?t _ => remember t; rewrite unfold_iter; subst end. rewrite unfold_iter; cbn. rewrite !bind_bind. ebind. econstructor; [reflexivity | intros [xa | xb] ? <-]. - rewrite ! bind_ret_l. rewrite bind_tau. etau. specialize (CIHL xa). cbn in CIHL. match goal with |- euttG _ _ _ _ _ ?t _ => remember t end. rewrite <- bind_ret_l. ebase. - rewrite ! bind_ret_l. rewrite tau_euttge. generalize xb. ecofix CIH'. intros ?. rewrite unfold_iter; cbn. match goal with |- euttG _ _ _ _ _ ?t _ => remember t; rewrite unfold_iter; subst end. cbn. rewrite !bind_bind. ebind. econstructor; [reflexivity | intros [xb' | xc] ? <-]. + rewrite !bind_ret_l. etau. + rewrite !bind_ret_l. eret. Qed.
imports: Coq(Classes.Morphisms Setoids.Setoid Relations.Relations) Paco(paco) ITree(Basics.Basics Basics.CategoryOps Basics.CategoryTheory Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Function Basics.HeterogeneousRelations Core.ITreeDefinition Core.ITreeMonad Core.KTree Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2)