fact: Definition lookup_def {E} `{mapE -< E} : K -> V -> itree E V := fun k v => ITree.bind (lookup k) (fun ov => Ret (match ov with | None => v | Some v' => v' end)).
imports: Coq(List) ITree(Basics.Basics Basics.CategoryOps Basics.MonadState Indexed.Sum Core.ITreeDefinition Core.Subevent Interp.Interp Events.State)