proposition: Lemma bind_bind : forall {E R S T} (s : itree E R) (k : R -> itree E S) (h : S -> itree E T), ITree.bind (ITree.bind s k) h ≈ ITree.bind s (fun r => ITree.bind (k r) h).
proof: Proof. intros; rewrite ITree.Eq.Eqit.bind_bind; 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)