proposition: Lemma eutt_eq_bind_gen {E R S T} (RS : R -> S -> Prop) (t: itree E T) (k1: T -> itree E R) (k2 : T -> itree E S) : (forall u, u ∈ t -> eutt RS (k1 u) (k2 u)) -> eutt RS (t >>= k1) (t >>= k2).
proof: Proof. intros; eapply eutt_clo_bind_gen. reflexivity. intros * IN _ <-; eauto. 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)