proposition: Lemma all_finite_Vis : forall E X R (e : E X) k, (forall x, all_finite (k x)) -> @all_finite E R (Vis e k).
proof: Proof. intros; econstructor 3; [reflexivity | eauto]. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)