proposition: Lemma interp_bind : forall {E F R S} (f : E ~> itree F) (t : itree E R) (k : R -> itree E S), interp f (ITree.bind t k) ≈ ITree.bind (interp f t) (fun r => interp f (k r)).
proof: Proof. intros; rewrite ITree.Interp.InterpFacts.interp_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)