diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index ea3802d..6400dd5 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -64,11 +64,11 @@ record Graph : Set where
     Adjacency-merge : Adjacency → Adjacency → Adjacency
     Adjacency-merge adj₁ adj₂ n₁ n₂ = adj₁ n₁ n₂ ++ˡ adj₂ n₁ n₂
 
-    through : Node → Adjacency → Adjacency
-    through n adj n₁ n₂ = cartesianProductWith _++_ (adj n₁ n) (adj n n₂) ++ˡ adj n₁ n₂
-
-    through-monotonic : ∀ adj n {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
-    through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
+    adj⁰ : Adjacency
+    adj⁰ n₁ n₂
+        with n₁ ≟ n₂
+    ... | yes refl = done ∷ []
+    ... | no _ = []
 
     seedWithEdges : ∀ (es : List Edge) →  (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency → Adjacency
     seedWithEdges es e∈es⇒e∈edges adj = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((step n₁n₂∈edges done) ∷_)) adj (mapWith∈ˡ es (λ {e} e∈es →  (e , e∈es⇒e∈edges e∈es)))
@@ -87,18 +87,18 @@ record Graph : Set where
     ...   | no _ | yes _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
     ...   | yes refl | no _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
 
-    adj⁰ : Adjacency
-    adj⁰ n₁ n₂
-        with n₁ ≟ n₂
-    ... | yes refl = done ∷ []
-    ... | no _ = []
-
     adj¹ : Adjacency
     adj¹ = seedWithEdges edges (λ x → x) adj⁰
 
     edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) →  (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
     edge∈adj¹ = e∈seedWithEdges (λ x → x)
 
+    through : Node → Adjacency → Adjacency
+    through n adj n₁ n₂ = cartesianProductWith _++_ (adj n₁ n) (adj n n₂) ++ˡ adj n₁ n₂
+
+    through-monotonic : ∀ adj n {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
+    through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
+
     throughAll : List Node → Adjacency
     throughAll = foldr through adj¹