proposition: Lemma any_finite_eutt_l {E A B R}: forall (t : itree E A) (u : itree E B), eutt R t u -> any_finite t -> any_finite u.
proof: Proof. intros * EQ FIN; revert u EQ. induction FIN; intros u2 EQ. - punfold EQ. red in EQ; rewrite H in EQ; clear H. remember (RetF a); genobs u2 ou. hinduction EQ before R; intros; try discriminate; eauto with itree. - punfold EQ; red in EQ; rewrite H in EQ; clear H. remember (TauF u); genobs u2 ou2. hinduction EQ before R; intros; try discriminate; pclearbot; inv Heqi; eauto with itree. - punfold EQ; red in EQ; rewrite H in EQ; clear H. remember (VisF e k); genobs u2 ou2. hinduction EQ before R; intros; try discriminate; pclearbot. + revert x FIN IHFIN. refine (match Heqi in _ = u return match u with VisF e0 k0 => _ | _ => False end with eq_refl => _ end). eauto with itree. + inv Heqi; eauto with itree. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)