fact: Definition submap_with (le : V -> V -> bool) (m1 m2 : map) : bool := fold (fun k_v (acc : bool) => if acc then let '(k,v) := k_v in match lookup k m2 with | None => false | Some v' => le v v' end else false) true m1.
imports: RelationClasses ExtLib.Structures.Monad ExtLib.Structures.Reducible