proposition: Lemma Leaf_Tau : forall E R a t, a ∈ (t : itree E R) -> a ∈ Tau t.
proof: Proof. intros; econstructor; [reflexivity | 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)