proposition: Lemma any_finite_trigger : forall E R (e: E R) (r: R), any_finite (ITree.trigger e).
proof: Proof. intros. apply any_finite_Vis with (x := r). auto with itree. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)