diff --git a/Map.agda b/Map.agda
index 96e05fc..98ec999 100644
--- a/Map.agda
+++ b/Map.agda
@@ -182,6 +182,42 @@ private module ImplInsert (f : B → B → B) where
     ...   | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
     ...   | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
 
+    insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
+                          k ∈k l → k ∈k insert k' v' l
+    insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'')
+        with (≡-dec-A k' k'')
+    ...   | yes _ = here k≡k''
+    ...   | no _ = here k≡k''
+    insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs)
+        with (≡-dec-A k' k'')
+    ...   | yes _ = there k∈kxs
+    ...   | no _ = there (insert-preserves-∈k k∈kxs)
+
+    union-preserves-∈k₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                          k ∈k l₁ → k ∈k (union l₁ l₂)
+    union-preserves-∈k₁ {k} {(k' , v') ∷ xs} {l₂} (here k≡k')
+        with ∈k-dec k (union xs l₂)
+    ...   | yes k∈kxsl₂ = insert-preserves-∈k k∈kxsl₂
+    ...   | no k∉kxsl₂ rewrite k≡k' = ∈-cong proj₁ (insert-fresh k∉kxsl₂)
+    union-preserves-∈k₁ {k} {(k' , v') ∷ xs} {l₂} (there k∈kxs) =
+        insert-preserves-∈k (union-preserves-∈k₁ k∈kxs)
+
+    union-preserves-∈k₂ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                          k ∈k l₂ → k ∈k (union l₁ l₂)
+    union-preserves-∈k₂ {k} {[]} {l₂} k∈kl₂ = k∈kl₂
+    union-preserves-∈k₂ {k} {(k' , v') ∷ xs} {l₂} k∈kl₂ =
+        insert-preserves-∈k (union-preserves-∈k₂ {l₁ = xs} k∈kl₂)
+
+    ∉-union-∉-either : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                       ¬ k ∈k union l₁ l₂ → ¬ k ∈k l₁ × ¬ k ∈k l₂
+    ∉-union-∉-either {k} {l₁} {l₂} k∉l₁l₂
+        with ∈k-dec k l₁
+    ...   | yes k∈kl₁ = absurd (k∉l₁l₂ (union-preserves-∈k₁ k∈kl₁))
+    ...   | no k∉kl₁ with ∈k-dec k l₂
+    ...         | yes k∈kl₂ = absurd (k∉l₁l₂ (union-preserves-∈k₂ {l₁ = l₁} k∈kl₂))
+    ...         | no k∉kl₂ = (k∉kl₁ , k∉kl₂)
+
+
     insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
                          ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l
     insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
@@ -193,12 +229,6 @@ private module ImplInsert (f : B → B → B) where
     ...   | yes _ = there k,v∈xs
     ...   | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
 
-    insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
-                          ¬ k ≡ k' → k ∈k l → k ∈k insert k' v' l
-    insert-preserves-∈k k≢k' k∈kl =
-        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)} →
                          ¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ union l₁ l₂
     union-preserves-∈₂ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
@@ -314,7 +344,7 @@ module _ (_≈_ : B → B → Set b) where
 
 module _ (f : B → 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
+             (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
@@ -332,12 +362,27 @@ module _ (f : B → B → B) where
                         (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₃
+        union-assoc₁ m₁@(l₁ , u₁) m₂@(l₂ , u₂) m₃@(l₃ , u₃) 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₃)) = {!!}
+        ...   | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
+                let (k∉ke₁ , k∉ke₂) = ImplInsert.∉-union-∉-either f {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
+                in (v₃ , (refl , ImplInsert.union-preserves-∈₂ f k∉ke₁ (ImplInsert.union-preserves-∈₂ f k∉ke₂ v₃∈e₃)))
+        ...   | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
+                (v₂ , (refl , ImplInsert.union-preserves-∈₂ f k∉ke₁ (ImplInsert.union-preserves-∈₁ f u₂ v₂∈e₂ k∉ke₃)))
+        ...   | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃))
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
+                (f v₂ v₃ , (refl , ImplInsert.union-preserves-∈₂ f k∉ke₁  (ImplInsert.union-combines f u₂ u₃ v₂∈e₂ v₃∈e₃)))
+        ...   | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
+                (v₁ , (refl , ImplInsert.union-preserves-∈₁ f u₁ v₁∈e₁ (ImplInsert.union-preserves-∉ f k∉ke₂ k∉ke₃)))
+        ...   | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
+                (f v₁ v₃ , (refl , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-preserves-∈₂ f k∉ke₂ v₃∈e₃)))
+        ...   | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
+                (f v₁ v₂ , (refl , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-preserves-∈₁ f u₂ v₂∈e₂ k∉ke₃)))
+        ...   | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
+                rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
+                (f v₁ (f v₂ v₃) , (f-assoc v₁ v₂ v₃ , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-combines f u₂ u₃ v₂∈e₂ v₃∈e₃)))