proposition: Lemma Leaf_Vis_inv : forall E X Y (e : E X) (k : _ -> itree E Y) b, b ∈ Vis e k -> exists x, b ∈ k x.
proof: Proof. intros * IN *; inv IN; cbn in *; try congruence. revert x H0. refine (match H in _ = u return match u with VisF e0 k0 => _ | RetF _ | TauF _ => False end with eq_refl => _ end). 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)