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. apply (unfold_bind (Tau t) k). Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)