proposition: Lemma any_finite_bind_inv_weak : forall {E R S} (t : itree E R) (k : R -> itree E S), any_finite (t >>= k) -> (any_finite t /\ exists x, any_finite (k x)).
proof: Proof. intros * FIN; apply any_finite_bind_inv in FIN as (?&?&?&?). split; eauto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)