proposition: Lemma spin_empty_Leaf: forall E X x, ~ x ∈ (@spin E X).
proof: Proof. intros * IN; apply Leaf_finite, spin_not_any_finite in IN; auto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)