proposition: Lemma unfold_bind {E R S} (t : itree E R) (k : R -> itree E S) : ITree.bind t k ≅ bind_ t k.
proof: Proof. apply observing_sub_eqit; constructor; reflexivity. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)