proposition: Lemma Leaf_eutt_l {E A B R}: forall (t : itree E A) (u : itree E B) (a : A), eutt R t u -> a ∈ t -> exists b, b ∈ u /\ R a b.
proof: Proof. intros * EQ FIN; revert u EQ. induction FIN; intros u2 EQ. - punfold EQ. red in EQ; rewrite H in EQ; clear H t. remember (RetF a); genobs u2 ou. hinduction EQ before R; intros; try now discriminate. + inv Heqi; eauto with itree. + edestruct IHEQ as (b & IN & HR); eauto with itree. - punfold EQ; red in EQ; rewrite H in EQ; clear H t. remember (TauF u); genobs u2 ou2. hinduction EQ before R; intros; try discriminate; pclearbot; inv Heqi. + edestruct IHFIN as (? & ? & ?); [ .. | eexists ]; eauto with itree. + eauto with itree. + edestruct IHEQ as (? & ? & ?); [ .. | eexists ]; eauto with itree. - punfold EQ; red in EQ; rewrite H in EQ; clear H t. 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 => _ | RetF _ | TauF _ => False end with eq_refl => _ end). intros. edestruct IHFIN as (? & ? & ?); [ | eexists ]; eauto with itree. + edestruct IHEQ as (? & ? & ?); [.. | exists x0 ]; 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)