proposition: Fact NotDFtk: ~ any_finite (t >>= k).
proof: Proof. intros abs. apply any_finite_bind_inv in abs as (FINt & b & IN & FINk). destruct b; cbn in *. - eapply spin_not_any_finite; eauto. - unfold t in IN. clear FINk FINt. inv IN; cbn in *; try congruence. dependent induction H. destruct x; cbn in *. apply Leaf_Ret_inv in H0; congruence. apply Leaf_finite in H0. eapply spin_not_any_finite; eauto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)