enrich
   map, 
   set-union
with
   functions 
       . ∪ . : Map[A, B] × Map[A, B] → Map[A, B];
       . \ . : Map[A, B] × Set[A] → Map[A, B];
       . \ . : Map[A, B] × Map[A, B] → Map[A, B];
       dom . : Map[A, B] → Set[A];
   
   predicates 
       . ⊥ . : Map[A, B] × Map[A, B];
   
   variables 
       h : Map[A, B];
       rs : Set[A];
       r : A;
       o : B;
       d : B;
       hP : Map[A, B] → Bool;
   
   
   axioms 
      dom: r ∈ dom h ↔ r ∈ h;
      used for: s, ls;
      
      uni-emp: h0 ∪ ∅ = h0;
      used for: s, ls;
      
      uni-put: h0 ⊥ h1 ⊦ h0 ∪ h1(r := o) = (h0 ∪ h1)(r := o);
      used for: ls;
      
      diff-emp: h0 \ ∅ = h0;
      used for: s, ls;
      
      diff-put: h0 \ h1(r := o) = (h0 -- r) \ h1;
      used for: s, ls;
      
      diffs-emp: h0 \ ∅ = h0;
      used for: s, ls;
      
      diffs-ins: h0 \ (rs ++ r) = (h0 -- r) \ rs;
      used for: s, ls;
      
      disj: h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1);
   
   
end enrich