proposition: Lemma subtree_image {E R} (t u: itree E R) x: subtree u t -> x ∈ u -> x ∈ t.
proof: Proof. intros * Hsub. induction Hsub; intros. - intros. rewrite <- H; auto. - apply IHHsub, Leaf_Tau, H. - eapply IHHsub, Leaf_Vis. rewrite H in H0; eauto. 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)