diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 33a0242..aaf3886 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -2,7 +2,7 @@ module Lattice.Builder where
 
 open import Lattice
 open import Equivalence
-open import Utils using (Unique; fins; fins-complete)
+open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; ¬Any-map; fins; fins-complete)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
@@ -13,7 +13,9 @@ open import Data.List.Membership.Propositional as MemProp using () renaming (_
 open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup)
+open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺)
 open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
+open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂)
 open import Data.Empty using (⊥; ⊥-elim)
@@ -47,14 +49,38 @@ record Graph : Set where
     done ++ p = p
     (step e p₁) ++ p₂ = step e (p₁ ++ p₂)
 
+    ++done : ∀ {n₁ n₂} (p : Path n₁ n₂) → p ++ done ≡ p
+    ++done done = refl
+    ++done (step e∈edges p) rewrite ++done p = refl
+
     interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
     interior done = []
     interior (step _ done) = []
     interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p
 
+    interior-extend : ∀ {n₁ n₂ n₃} → (p : Path n₁ n₂) →  (n₂,n₃∈edges : (n₂ , n₃) ∈ˡ edges) →
+                      let p' = (p ++ (step n₂,n₃∈edges done))
+                      in (interior p' ≡ interior p) ⊎ (interior p' ≡ interior p ++ˡ (n₂ ∷ []))
+    interior-extend done _ = inj₁ refl
+    interior-extend (step n₁,n₂∈edges done) n₂n₃∈edges = inj₂ refl
+    interior-extend {n₂ = n₂} (step {n₂ = n} n₁,n∈edges p@(step _ _)) n₂n₃∈edges
+        with p ++ (step n₂n₃∈edges done) | interior-extend p n₂n₃∈edges
+    ...   | done | inj₁ []≡intp rewrite sym []≡intp = inj₁ refl
+    ...   | done | inj₂ []=intp++[n₂] with () ← ++ˡ-conicalʳ (interior p) (n₂ ∷ []) (sym []=intp++[n₂])
+    ...   | step _ p | inj₁ IH rewrite IH = inj₁ refl
+    ...   | step _ p | inj₂ IH rewrite IH = inj₂ refl
+
     SimpleWalkVia : List Node → Node → Node → Set
     SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (λ n → n ∈ˡ ns) (interior p))
 
+    SimpleWalk-extend : ∀ {n₁ n₂ n₃ ns} →  (w : SimpleWalkVia ns n₁ n₂) → (n₂ , n₃) ∈ˡ edges →  All (λ nʷ →  ¬ nʷ ≡ n₂) (interior (proj₁ w)) → n₂ ∈ˡ ns → SimpleWalkVia ns n₁ n₃
+    SimpleWalk-extend (p , (Unique-intp , intp⊆ns)) n₂,n₃∈edges w≢n₂ n₂∈ns
+        with p ++ (step n₂,n₃∈edges done) | interior-extend p n₂,n₃∈edges
+    ...   | p' | inj₁ intp'≡intp rewrite sym intp'≡intp = (p' , Unique-intp , intp⊆ns)
+    ...   | p' | inj₂ intp'≡intp++[n₂]
+            with intp++[n₂]⊆ns ←  ++ˡ⁺ intp⊆ns (n₂∈ns ∷ [])
+            rewrite sym intp'≡intp++[n₂] = (p' , (subst Unique (sym intp'≡intp++[n₂]) (Unique-append (¬Any-map sym (All¬-¬Any w≢n₂)) Unique-intp) , intp++[n₂]⊆ns))
+
     postulate SplitSimpleWalkVia : ∀ {n n₁ n₂ ns} (w : SimpleWalkVia (n ∷ ns) n₁ n₂) →  (Σ (SimpleWalkVia ns n₁ n × SimpleWalkVia ns n n₂) λ (w₁ , w₂) → proj₁ w₁ ++ proj₁ w₂ ≡ proj₁ w) ⊎ (Σ (SimpleWalkVia ns n₁ n₂) λ w' → proj₁ w' ≡ proj₁ w)
 
     postulate findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) →  (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w →  ¬ proj₁ w ≡ done))
diff --git a/Utils.agda b/Utils.agda
index 0a0ce3a..d9c3056 100644
--- a/Utils.agda
+++ b/Utils.agda
@@ -9,7 +9,7 @@ open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; fil
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
 open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
-open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there) -- TODO: re-export these with nicer names from map
 open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
@@ -52,6 +52,9 @@ All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x
 All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
 All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
 
+¬Any-map : ∀ {p₁ p₂ c} {C : Set c} {P₁ : C → Set p₁} {P₂ : C → Set p₂} {l : List C} → (∀ {x} → P₁ x → P₂ x) → ¬ Any P₂ l → ¬ Any P₁ l
+¬Any-map f ¬Any-P₂ Any-P₁ = ¬Any-P₂ (Any.map f Any-P₁)
+
 All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (there c∈xs) = All-single ps c∈xs