proposition: Lemma Leaf_Vis : forall E X Y (e : E X) (k : _ -> itree E Y) b x, b ∈ (k x) -> b ∈ (Vis e k).
proof: Proof. intros * IN; econstructor 3; [reflexivity | 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)