proposition: Lemma eutt_clo_bind {U1 U2 UU} t1 t2 k1 k2 (EQT: @eutt E U1 U2 UU t1 t2) (EQK: forall u1 u2, UU u1 u2 -> eutt RR (k1 u1) (k2 u2)): eutt RR (ITree.bind t1 k1) (ITree.bind t2 k2).
proof: Proof. intros. ginit. guclo eqit_clo_bind. econstructor; eauto. intros; subst. gfinal. right. apply EQK. 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)