proposition: Lemma eqit_clo_bind_gen : forall {E} {R1 R2} (RR : R1 -> R2 -> Prop) {U1 U2} {UU : U1 -> U2 -> Prop} b1 b2 (t1 : itree E U1) (t2 : itree E U2) (k1 : U1 -> itree E R1) (k2 : U2 -> itree E R2), eqit UU b1 b2 t1 t2 -> (forall (u1 : U1) (u2 : U2), u1 ∈ t1 -> u2 ∈ t2 -> UU u1 u2 -> eqit RR b1 b2 (k1 u1) (k2 u2)) -> eqit RR b1 b2 (x <- t1;; k1 x) (x <- t2;; k2 x).
proof: Proof. intros. ginit. guclo (@eqit_Leaf_clo_bind E R1 R2). econstructor; eauto. intros * IN1 IN2 HR. gfinal; right. apply H0; auto. 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)