proposition: Lemma all_finite_bind_weak : forall {E R S} (t : itree E R) (k : R -> itree E S), all_finite t -> (forall x, all_finite (k x)) -> all_finite (t >>= k).
proof: Proof. intros; apply all_finite_bind; auto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)