proposition: Lemma unfold_forever_ {E R S} (t: itree E R): observing eq (@ITree.forever E R S t) (ITree.bind t (fun _ => Tau (ITree.forever t))).
proof: Proof. econstructor. reflexivity. Qed.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)