proposition: Lemma eutt_eq_bind' {E U R} (t1 t2: itree E U) (k1 k2: U -> itree E R): t1 ≈ t2 -> (forall u, (k1 u) ≈ (k2 u)) -> (ITree.bind t1 k1) ≈ (ITree.bind t2 k2).
proof: Proof. intros -> Hk. now apply eutt_eq_bind. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)