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