proposition: Lemma all_finite_bind_inv : forall {E R S} (t : itree E R) (k : R -> itree E S), all_finite (t >>= k) -> (all_finite t /\ forall x, x ∈ t -> all_finite (k x)).
proof: Proof. intros E R S. cut (forall (u : itree E S), all_finite u -> forall (t : itree E R) k, u ≈ t >>= k -> (all_finite t /\ forall x, x ∈ t -> all_finite (k x))). intros LEM * FIN; eapply LEM; eauto; reflexivity. induction 1; intros * EQ. - rewrite (itree_eta t), H in EQ; clear H t. symmetry in EQ; apply eqit_inv_bind_ret in EQ as (? & EQt & EQk). rewrite EQt; split; auto with itree. intros z IN. rewrite EQt in IN; apply Leaf_Ret_inv in IN; subst. rewrite EQk; auto with itree. - rewrite (itree_eta t), H in EQ; clear H t. rewrite tau_eutt in EQ. eauto. - rewrite (itree_eta t), H in EQ; clear H t. symmetry in EQ; apply eutt_inv_bind_vis in EQ. destruct EQ as [(kca & EQ & EQk) | (?a & EQ & EQk)]. + rewrite EQ. split. apply all_finite_Vis. intros ?; eapply H1; symmetry; eauto. intros x IN. rewrite EQ in IN. apply Leaf_Vis_inv in IN as (y & IN). edestruct H1 as (_ & H). symmetry in EQk; exact (EQk y). apply H, IN. + rewrite EQ; split; auto with itree. intros y IN. rewrite EQ in IN; apply Leaf_Ret_inv in IN; subst. rewrite EQk. 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)