diff --git a/Map.agda b/Map.agda
index 98ec999..9a9250d 100644
--- a/Map.agda
+++ b/Map.agda
@@ -386,3 +386,14 @@ module _ (f : B → B → B) where
         ...   | (_ , (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₃)))
+
+        union-assoc₂ : ∀ (m₁ m₂ m₃ : Map) → subset (_≡_) (union f m₁ (union f m₂ m₃)) (union f (union f m₁ 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₁ (in₂ k∉e₂ (single {v₃} v₁∈e₃)) , v₃∈m₁m₂₃)) = {!!}
+        ...   | (_ , (in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉e₃) , v₂∈m₁m₂₃)) = {!!}
+        ...   | (_ , (in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₁∈e₃)) , v₂v₃∈m₁m₂₃)) = {!!}
+        ...   | (_ , (in₁ (single {v₁} v₁∈e₁) k∉ke₁₂ , v₁∈m₁m₂₃)) = {!!}
+        ...   | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉e₂ (single {v₃} v₁∈e₃)) , v₁v₃∈m₁m₂₃)) = {!!}
+        ...   | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉e₃) , v₁v₂∈m₁m₂₃)) = {!!}
+        ...   | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₁∈e₃)) , v₁v₂v₃∈m₁m₂₃)) = {!!}