proposition: Lemma bind_bind {E R S T} : forall (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. ginit. pcofix CIH. intros. lazymatch goal with | [ |- _ (ITree.bind ?t1 _) ?t2 ] => rewrite (itree_eta_ t1), (itree_eta_ t2); cbn end. lazymatch goal with | [ |- _ ?t0 _ ] => rewrite (itree_eta_ t0); cbn end. destruct (observe s); cbn. 1: apply reflexivity. all: gstep; constructor; eauto with paco itree. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)