proposition: Lemma Leaf_Tau_inv : forall E R (u : itree E R) b, b ∈ Tau u -> b ∈ u.
proof: Proof. intros * IN; inv IN; cbn in *; try congruence. 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)