proposition: Lemma finite_Leaf : forall E R (t : itree E R), any_finite t -> exists x, x ∈ t.
proof: Proof. intros * FIN; induction FIN. 1: exists a; rewrite itree_eta, H; eauto with itree. all: destruct IHFIN; eauto with itree. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)