proposition: Lemma bind_tau {E R} U t (k: U -> itree E R) : ITree.bind (Tau t) k ≈ Tau (ITree.bind t k).
proof: Proof. rewrite bind_tau_. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion ITree(Eq.Eqit Eq.UpToTaus Interp.InterpFacts Interp.RecursionFacts)