proposition: Fact fail_not_any_finite: ~ any_finite fail.
proof: Proof. unfold fail; intros FIN. apply any_finite_Vis_inv in FIN as ([] & ? & ?). Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)