proposition: Lemma spin_not_any_finite: forall E X, ~ any_finite (@spin E X).
proof: Proof. intros * FIN; remember spin as t; revert Heqt; induction FIN; intros ->; unfold observe in H; cbn in H; inv H; auto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)