proposition: Lemma Leaf_translate_inv {E F R} `{Inj: E -< F}: forall (t: itree E R) v, v ∈ translate (@subevent E F _) t -> v ∈ t.
proof: Proof. intros. rewrite translate_to_interp in H. eapply Leaf_interp_inv; 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)