proposition: Lemma Leaf_bind : forall {E R S} (t : itree E R) (k : R -> itree E S) a b, b ∈ t -> a ∈ k b -> a ∈ t >>= k.
proof: Proof. intros * INt INk; induction INt. - rewrite (itree_eta t), H, bind_ret_l; auto. - rewrite (itree_eta t), H, tau_eutt; auto. - rewrite (itree_eta t), H, bind_vis. apply Leaf_Vis with x; 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)