Some theorems about omaps.
Theorem: lookup-of-update
(defthm omap::lookup-of-update (equal (omap::lookup key (omap::update key1 val map)) (if (equal key key1) val (omap::lookup key map))))