proposition: Lemma Leaf_Ret_inv : forall E R (a b : R), Leaf (E := E) b (Ret a) -> b = a.
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)