proposition: Lemma Leaf_eutt_r {E A B R}: forall (t : itree E A) (u : itree E B) (b : B), eutt R t u -> b ∈ u -> exists a, a ∈ t /\ R a b.
proof: Proof. intros * EQ FIN. apply eqit_flip in EQ. revert EQ FIN. apply @Leaf_eutt_l. 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)