proposition: Lemma unfold_aloop_ {E A B} (f : A -> itree E (A + B)) (x : A) : observing eq (ITree.iter f x) (ITree.bind (f x) (fun lr => ITree.on_left lr l (Tau (ITree.iter f l)))).
proof: Proof. constructor; reflexivity. Qed.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)