fact: Definition lookup {E} `{mapE -< E} : K -> itree E (option V) := embed Lookup.
imports: Coq(List) ITree(Basics.Basics Basics.CategoryOps Basics.MonadState Indexed.Sum Core.ITreeDefinition Core.Subevent Interp.Interp Events.State)