proposition: Lemma all_finite_Tau_inv : forall E R t, @all_finite E R (Tau t) -> all_finite t.
proof: Proof. intros * FIN; inv FIN; cbn in *; congruence. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)