proposition: Lemma any_finite_bind_inv : forall {E R S} (t : itree E R) (k : R -> itree E S), any_finite (t >>= k) -> (any_finite t /\ exists x, x ∈ t /\ any_finite (k x)).
proof: Proof. intros * FIN; remember (ITree.bind t k) as u. revert t k Hequ. induction FIN; intros t' k' ->; rename t' into t. - unfold observe in H; cbn in H. desobs t EQ; cbn in *; try congruence. split; eauto with itree. - unfold observe in H; cbn in H. desobs t EQ; cbn in *; try congruence. split; eauto with itree. inversion H; clear H; symmetry in H1. edestruct IHFIN as (? & ? & ? & ?). apply H1. split; eauto with itree. - unfold observe in H; cbn in H. desobs t EQ; cbn in *; try congruence. split; eauto with itree. revert x FIN IHFIN. refine (match H in _ = u return match u with VisF e0 k0 => _ | _ => False end with eq_refl => _ end). intros. edestruct IHFIN as (? & ? & ? & ?); [ reflexivity | ]. split; 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)