proposition: Lemma any_finite_Vis_inv : forall E X R (e : E X) k, @any_finite E R (Vis e k) -> exists x, any_finite (k x).
proof: Proof. intros * FIN; inv FIN; cbn in *; try congruence. revert x H0. refine (match H in _ = u return match u with VisF e0 k0 => _ | _ => False end with eq_refl => _ end). eauto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)