proposition: Lemma Leaf_bind_inv : forall {E R S} (t : itree E R) (k : R -> itree E S) a, a ∈ t >>= k -> exists b, b ∈ t /\ a ∈ k b.
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. exists r; auto with itree. - unfold observe in H; cbn in H. desobs t EQ; cbn in *; try congruence; [ eexists; eauto with itree | ]. inversion H; clear H; symmetry in H1. edestruct IHFIN as (? & ? & ?); [ eauto | eexists; eauto with itree ]. - unfold observe in H; cbn in H. desobs t EQ; cbn in *; try congruence; [ eexists; eauto with itree | ]. revert x FIN IHFIN. refine (match H in _ = u return match u with VisF e0 k0 => _ | RetF _ | TauF _ => False end with eq_refl => _ end). intros. edestruct IHFIN as (? & ? & ?); [ reflexivity | eexists; eauto with itree ]. Qed.
imports: ITree(Basics.Utils Basics.HeterogeneousRelations ITree Eq.Shallow Eq.Eqit Interp.InterpFacts Events.State Events.StateFacts Props.HasPost) Paco(paco) Coq(Morphisms Basics Program.Equality)