diff --git a/Map.agda b/Map.agda
index 72e3a21..96e05fc 100644
--- a/Map.agda
+++ b/Map.agda
@@ -199,25 +199,25 @@ private module ImplInsert (f : B → B → B) where
         let (v , k,v∈l) = locate k∈kl
         in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
 
-    union-preserves-∈₁ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
+    union-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
                          ¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ union l₁ l₂
-    union-preserves-∈₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
-    union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ =
-        let recursion = union-preserves-∈₁ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂
+    union-preserves-∈₂ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
+    union-preserves-∈₂ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ =
+        let recursion = union-preserves-∈₂ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂
         in insert-preserves-∈ (λ k≡k' → k∉kl₁ (here k≡k')) recursion
 
-    union-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
+    union-preserves-∈₁ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
                          Unique (keys l₁) → (k , v) ∈ l₁ → ¬ k ∈k l₂ → (k , v) ∈ union l₁ l₂
-    union-preserves-∈₂ {k} {v} {(k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
+    union-preserves-∈₁ {k} {v} {(k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
         insert-preserves-∈ k≢k' k,v∈mxs₁l
         where
-            k,v∈mxs₁l = union-preserves-∈₂ uxs₁ k,v∈xs₁ k∉kl₂
+            k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂
 
             k≢k' : ¬ k ≡ k'
             k≢k' with ≡-dec-A k k'
             ...    | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
             ...    | no  k≢k' = k≢k'
-    union-preserves-∈₂ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
+    union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
         rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' =
         insert-fresh (union-preserves-∉ (All¬-¬Any k'≢xs₁) k∉kl₂)
 
@@ -238,7 +238,7 @@ private module ImplInsert (f : B → B → B) where
                      (k , v₁) ∈ l₁ → (k , v₂) ∈ l₂ → (k , f v₁ v₂) ∈ union l₁ l₂
     union-combines {l₁ = (k' , v) ∷ xs₁} {l₂} (push k'≢xs₁ uxs₁) ul₂ (here k,v₁≡k',v) k,v₂∈l₂
         rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) =
-        insert-combines (union-preserves-Unique xs₁ l₂ ul₂) (union-preserves-∈₁ (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
+        insert-combines (union-preserves-Unique xs₁ l₂ ul₂) (union-preserves-∈₂ (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
     union-combines {k} {l₁ = (k' , v) ∷ xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ =
         insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
         where
@@ -296,10 +296,10 @@ module _ (f : B → B → B) where
             in  (f v₁ v₂ , (bothᵘ g₁ g₂ , union-combines (proj₂ ⟦ e₁ ⟧) (proj₂ ⟦ e₂ ⟧) k,v₁∈e₁ k,v₂∈e₂))
     ...   | yes k∈ke₁ | no k∉ke₂ =
             let (v₁ , (g₁ , k,v₁∈e₁)) = Expr-Provenance k e₁ k∈ke₁
-            in (v₁ , (in₁ g₁ k∉ke₂ , union-preserves-∈₂ (proj₂ ⟦ e₁ ⟧) k,v₁∈e₁ k∉ke₂))
+            in (v₁ , (in₁ g₁ k∉ke₂ , union-preserves-∈₁ (proj₂ ⟦ e₁ ⟧) k,v₁∈e₁ k∉ke₂))
     ...   | no k∉ke₁ | yes k∈ke₂ =
             let (v₂ , (g₂ , k,v₂∈e₂)) = Expr-Provenance k e₂ k∈ke₂
-            in (v₂ , (in₂ k∉ke₁ g₂ , union-preserves-∈₁ k∉ke₁ k,v₂∈e₂))
+            in (v₂ , (in₂ k∉ke₁ g₂ , union-preserves-∈₂ k∉ke₁ k,v₂∈e₂))
     ...   | no k∉ke₁ | no k∉ke₂  = absurd (union-preserves-∉ k∉ke₁ k∉ke₂ k∈ke₁e₂)
 
 
@@ -313,7 +313,8 @@ module _ (_≈_ : B → B → Set b) where
     lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁
 
 module _ (f : B → B → B) where
-    module _ (f-comm : ∀ (b₁ b₂ : B) → f b₁ b₂ ≡ f b₂ b₁) where
+    module _ (f-comm : ∀ (b₁ b₂ : B) → f b₁ b₂ ≡ f b₂ b₁)
+             (f-assoc : ∀ (b₁ b₂ b₃ : B) → f (f b₁ b₂) b₃ ≡ f b₁ (f b₁ b₂)) where
         union-comm : ∀ (m₁ m₂ : Map) → lift (_≡_) (union f m₁ m₂) (union f m₂ m₁)
         union-comm m₁ m₂ = (union-comm-subset m₁ m₂ , union-comm-subset m₂ m₁)
             where
@@ -325,7 +326,18 @@ module _ (f : B → B → B) where
                         (f v₂ v₁ , (f-comm v₁ v₂ , ImplInsert.union-combines f u₂ u₁ v₂∈m₂ v₁∈m₁))
                 ...   | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
                         rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
-                        (v₁ , (refl , ImplInsert.union-preserves-∈₁ f k∉km₂ v₁∈m₁))
+                        (v₁ , (refl , ImplInsert.union-preserves-∈₂ f k∉km₂ v₁∈m₁))
                 ...   | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
                         rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
-                        (v₂ , (refl , ImplInsert.union-preserves-∈₂ f u₂ v₂∈m₂ k∉km₁))
+                        (v₂ , (refl , ImplInsert.union-preserves-∈₁ f u₂ v₂∈m₂ k∉km₁))
+
+        union-assoc₁ : ∀ (m₁ m₂ m₃ : Map) → subset (_≡_) (union f (union f m₁ m₂) m₃) (union f m₁ (union f m₂ m₃))
+        union-assoc₁ m₁ m₂ m₃ k v k,v∈m₁₂m₃
+            with Expr-Provenance f k (((` m₁) ∪ (` m₂)) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
+        ...   | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃)) = {!!}
+        ...   | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke3 , v₂∈m₁₂m₃)) = {!!}
+        ...   | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃)) = {!!}
+        ...   | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃)) = {!!}
+        ...   | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃)) = {!!}
+        ...   | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃) = {!!}
+        ...   | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃)) = {!!}