proposition: Lemma iter_codiagonal_ktree {E A B} (f : ktree E A (A + (A + B))) (a0 : A) : iter (iter f) a0 ≅ iter (C := ktree _) (fun a => ITree.bind (f a) (fun r => match r with | inl a' => Ret (inl a') | inr (inl a') => Ret (inl a') | inr (inr b) => Ret (inr b) end)) a0.
proof: Proof. revert a0. ginit. pcofix CIH. intros. rewrite unfold_iter_ktree. rewrite (unfold_iter_ktree (fun _ => _ _ _)). rewrite unfold_iter_ktree, !bind_bind. guclo eqit_clo_bind. econstructor. reflexivity. intros [| []] ? []. - rewrite bind_ret_l, bind_tau. gstep. constructor. revert a. pcofix CIH'. intros. rewrite unfold_iter_ktree. rewrite (unfold_iter_ktree (fun _ => _ _ _)). rewrite !bind_bind. guclo eqit_clo_bind. econstructor. reflexivity. intros [| []] ? []. + rewrite bind_tau, bind_ret_l. gstep; constructor; auto with paco. + rewrite 2 bind_ret_l. gstep; constructor; auto with paco. + rewrite 2 bind_ret_l. gstep; constructor; auto. - rewrite 2 bind_ret_l. gstep; constructor; auto with paco. - rewrite 2 bind_ret_l. gstep; reflexivity. 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)