diff --git a/Map.agda b/Map.agda
index 6f41ba8..af0e3cd 100644
--- a/Map.agda
+++ b/Map.agda
@@ -152,35 +152,35 @@ private module ImplInsert (f : B → B → B) where
     merge-preserves-Unique ((k₁ , v₁) ∷ xs₁) l₂ u₂ =
         insert-preserves-Unique (merge-preserves-Unique xs₁ l₂ u₂)
 
-    insert-preserves-∈-right : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
+    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-∈-right {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
+    insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
         rewrite sym k,v=x with ≡-dec-A k' k
     ...   | yes k'≡k = absurd (k≢k' (sym k'≡k))
     ...   | no _ = here refl
-    insert-preserves-∈-right {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs)
+    insert-preserves-∈ {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs)
         with ≡-dec-A k' k''
     ...   | yes _ = there k,v∈xs
-    ...   | no _ = there (insert-preserves-∈-right k≢k' k,v∈xs)
+    ...   | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
 
-    insert-preserves-∈k-right : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
+    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-right k≢k' k∈kl =
+    insert-preserves-∈k k≢k' k∈kl =
         let (v , k,v∈l) = locate k∈kl
-        in ∈-cong proj₁ (insert-preserves-∈-right k≢k' k,v∈l)
+        in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
 
-    insert-preserves-∉-right : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
+    insert-preserves-∉ : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
                                   ¬ k ≡ k' → ¬ k ∈k l → ¬ k ∈k insert k' v' l
-    insert-preserves-∉-right {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
-    insert-preserves-∉-right {l = []} k≢k' k∉kl (there ())
-    insert-preserves-∉-right {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil
+    insert-preserves-∉ {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
+    insert-preserves-∉ {l = []} k≢k' k∉kl (there ())
+    insert-preserves-∉ {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil
         with ≡-dec-A k k''
     ...   | yes k≡k'' = k∉kl (here k≡k'')
     ...   | no k≢k'' with ≡-dec-A k' k'' | k∈kil
     ...       | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
     ...       | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
     ...       | no k'≢k''  | here k≡k'' = k∉kl (here k≡k'')
-    ...       | no k'≢k''  | there k∈kxs = insert-preserves-∉-right k≢k'
+    ...       | no k'≢k''  | there k∈kxs = insert-preserves-∉ k≢k'
                                            (λ k∈kxs → k∉kl (there k∈kxs)) k∈kxs
 
     merge-preserves-∉ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
@@ -189,14 +189,14 @@ private module ImplInsert (f : B → B → B) where
     merge-preserves-∉ {k} {(k' , v') ∷ xs₁} k∉kl₁ k∉kl₂
         with ≡-dec-A k k'
     ...   | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
-    ...   | no k≢k' = insert-preserves-∉-right k≢k' (merge-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
+    ...   | no k≢k' = insert-preserves-∉ k≢k' (merge-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
 
     merge-preserves-keys₁ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
                             ¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ merge l₁ l₂
     merge-preserves-keys₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
     merge-preserves-keys₁ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ =
         let recursion = merge-preserves-keys₁ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂
-        in insert-preserves-∈-right (λ k≡k' → k∉kl₁ (here k≡k')) recursion
+        in insert-preserves-∈ (λ k≡k' → k∉kl₁ (here k≡k')) recursion
 
     insert-fresh : ∀ {k : A} {v : B} {l : List (A × B)} →
                                  ¬ k ∈k l → (k , v) ∈ insert k v l
@@ -209,7 +209,7 @@ private module ImplInsert (f : B → B → B) where
     merge-preserves-keys₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
                             Unique (keys l₁) → (k , v) ∈ l₁ → ¬ k ∈k l₂ → (k , v) ∈ merge l₁ l₂
     merge-preserves-keys₂ {k} {v} {(k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
-        insert-preserves-∈-right k≢k' k,v∈mxs₁l
+        insert-preserves-∈ k≢k' k,v∈mxs₁l
         where
             k,v∈mxs₁l = merge-preserves-keys₂ uxs₁ k,v∈xs₁ k∉kl₂
 
@@ -240,7 +240,7 @@ private module ImplInsert (f : B → B → B) where
         rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) =
         insert-combines (merge-preserves-Unique xs₁ l₂ ul₂) (merge-preserves-keys₁ (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
     merge-combines {k} {l₁ = (k' , v) ∷ xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ =
-        insert-preserves-∈-right k≢k' (merge-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
+        insert-preserves-∈ k≢k' (merge-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
         where
             k≢k' : ¬ k ≡ k'
             k≢k' with ≡-dec-A k k'