proposition: Lemma unfold_iter {E A B} (f : A -> itree E (A + B)) (x : A) : (ITree.iter f x) ≅ ITree.bind (f x) (fun lr => ITree.on_left lr l (Tau (ITree.iter f l))).
proof: Proof. rewrite unfold_aloop_. reflexivity. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)