From af0066eaa75c01705cdbe0973261e3446a46665a Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 30 Jul 2023 13:49:38 -0700
Subject: [PATCH] Rearrange a few functions

---
 Map.agda | 52 ++++++++++++++++++++++++++--------------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/Map.agda b/Map.agda
index a13707b..ba47d91 100644
--- a/Map.agda
+++ b/Map.agda
@@ -152,22 +152,13 @@ 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-∈ : ∀ {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)
-        rewrite sym k,v=x with ≡-dec-A k' k
-    ...   | yes k'≡k = absurd (k≢k' (sym k'≡k))
-    ...   | no _ = here refl
-    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-∈ 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)
+    insert-fresh : ∀ {k : A} {v : B} {l : List (A × B)} →
+                                 ¬ k ∈k l → (k , v) ∈ insert k v l
+    insert-fresh {l = []} k∉kl = here refl
+    insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl
+        with ≡-dec-A k k'
+    ...   | yes k≡k' = absurd (k∉kl (here k≡k'))
+    ...   | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs)))
 
     insert-preserves-∉k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
                                   ¬ k ≡ k' → ¬ k ∈k l → ¬ k ∈k insert k' v' l
@@ -191,23 +182,32 @@ 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' (merge-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) 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)
+        rewrite sym k,v=x with ≡-dec-A k' k
+    ...   | yes k'≡k = absurd (k≢k' (sym k'≡k))
+    ...   | no _ = here refl
+    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-∈ 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)
+
     merge-preserves-∈₁ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
-                            ¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ merge l₁ l₂
+                         ¬ k ∈k l₁ → (k , v) ∈ l₂ → (k , v) ∈ merge l₁ l₂
     merge-preserves-∈₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
     merge-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ =
         let recursion = merge-preserves-∈₁ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂
         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
-    insert-fresh {l = []} k∉kl = here refl
-    insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl
-        with ≡-dec-A k k'
-    ...   | yes k≡k' = absurd (k∉kl (here k≡k'))
-    ...   | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs)))
-
     merge-preserves-∈₂ : ∀ {k : A} {v : B} {l₁ l₂ : List (A × B)} →
-                            Unique (keys l₁) → (k , v) ∈ l₁ → ¬ k ∈k l₂ → (k , v) ∈ merge l₁ l₂
+                         Unique (keys l₁) → (k , v) ∈ l₁ → ¬ k ∈k l₂ → (k , v) ∈ merge l₁ l₂
     merge-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