proposition: Lemma eutt_clo_bind_gen : forall {E} {R1 R2} (RR : R1 -> R2 -> Prop) {U1 U2} {UU : U1 -> U2 -> Prop} (t1 : itree E U1) (t2 : itree E U2) (k1 : U1 -> itree E R1) (k2 : U2 -> itree E R2), eutt UU t1 t2 -> (forall (u1 : U1) (u2 : U2), u1 ∈ t1 -> u2 ∈ t2 -> UU u1 u2 -> eutt RR (k1 u1) (k2 u2)) -> eutt RR (x <- t1;; k1 x) (x <- t2;; k2 x).
proof: Proof. intros *; apply eqit_clo_bind_gen. Qed.
imports: ITree(Basics.Utils Basics.HeterogeneousRelations ITree Eq.Shallow Eq.Eqit Interp.InterpFacts Events.State Events.StateFacts Props.HasPost) Paco(paco) Coq(Morphisms Basics Program.Equality)