diff --git a/Map.agda b/Map.agda
index c0bd28e..f8ae3f7 100644
--- a/Map.agda
+++ b/Map.agda
@@ -411,7 +411,7 @@ module _ (_≈_ : B → B → Set b) where
                             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₃ , I.union-combines u₁ (I.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
 
-                    union-assoc₂ : subset (union f m₁ (union f m₂ m₃)) (union f (union f m₁ m₂) m₃) 
+                    union-assoc₂ : subset (union f m₁ (union f m₂ m₃)) (union f (union f m₁ m₂) m₃)
                     union-assoc₂ 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∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))