Check if an omap is a submap of another omap.
This is true when every key in the first omap is also in the second omap, and the two omaps agree on the common keys.
This is similar to subset for osets.
(defun submap (sub sup) (declare (xargs :guard (and (mapp sub) (mapp sup)))) (let ((__function__ 'submap)) (declare (ignorable __function__)) (cond ((empty sub) t) (t (mv-let (key val) (head sub) (and (equal (in key sup) (cons key val)) (submap (tail sub) sup)))))))
(defthm booleanp-of-submap (b* ((yes/no (submap sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm submap-when-left-empty (implies (empty sub) (submap sub sup)))
(defthm submap-when-right-empty (implies (empty sup) (equal (submap sub sup) (empty sub))))