Remove a key, and associated value, from an omap.
This is similar to set::delete for osets.
(defun delete (key map) (declare (xargs :guard (mapp map))) (let ((__function__ 'delete)) (declare (ignorable __function__)) (cond ((empty map) nil) (t (mv-let (key0 val0) (head map) (cond ((equal key key0) (tail map)) (t (update key0 val0 (delete key (tail map))))))))))
(defthm mapp-of-delete (b* ((map1 (delete key map))) (mapp map1)) :rule-classes :rewrite)
(defthm delete-when-empty (implies (empty map) (equal (delete key map) nil)))