proposition: Lemma any_finite_bind : forall {E R S} (t : itree E R) (k : R -> itree E S) x, x ∈ t -> any_finite (k x) -> any_finite (t >>= k).
proof: Proof. intros * IN FIN; induction IN. - rewrite (itree_eta t), H, bind_ret_l; auto. - rewrite unfold_bind, H, tau_eutt; eauto. - rewrite unfold_bind, H. eapply any_finite_Vis; eauto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)