proposition: Lemma any_finite_eutt_r {E A B R}: forall (t : itree E A) (u : itree E B), eutt R t u -> any_finite u -> any_finite t.
proof: Proof. intros * EQ. apply eqit_flip in EQ. revert EQ. apply any_finite_eutt_l. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)