proposition: Lemma finite_leaf_non_interactive : forall X (t: itree void1 X), all_finite t <-> (exists x, x ∈ t).
proof: Proof. intros *. rewrite finite_non_interactive. split; [ eauto using finite_Leaf | intros []; eauto using Leaf_finite ]. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)