proposition: Lemma unfold_forever {E R S} (t : itree E R) : @ITree.forever E R S t ≅ ITree.bind t (fun _ => Tau (ITree.forever t)).
proof: Proof. rewrite itree_eta, (itree_eta (ITree.bind _ _)). 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)