proposition: Lemma eq_itree_clo_bind {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop) {U1 U2 UU} t1 t2 k1 k2 (EQT: @eq_itree E U1 U2 UU t1 t2) (EQK: forall u1 u2, UU u1 u2 -> eq_itree RR (k1 u1) (k2 u2)): eq_itree RR (ITree.bind t1 k1) (ITree.bind t2 k2).
proof: Proof. eapply eqit_bind'; eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)