proposition: Lemma unfold_iter_ktree {E A B} (f : ktree E A (A + B)) (a0 : A) : iter f a0 ≅ ITree.bind (f a0) (fun ab => match ab with | inl a => Tau (iter f a) | inr b => Ret b end).
proof: Proof. apply unfold_iter. 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)