diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda
index 89cd2d0..75dcc31 100644
--- a/Minesweeper/Board.agda
+++ b/Minesweeper/Board.agda
@@ -22,7 +22,7 @@ lookup : ∀ {A bounds} → Coords bounds → Board A bounds → A
 lookup (x , y) grid = Vec.lookup x (Vec.lookup y grid)
 
 _[_]≔_ : ∀ {A bounds} → Board A bounds → Coords bounds → A → Board A bounds
-grid [ (x , y) ]≔ value = grid Vec.[ y ]≔ (Vec.lookup y grid Vec.[ x ]≔ value)
+grid [ (x , y) ]≔ value = Vec.updateAt y (Vec._[ x ]≔ value) grid
 
 _Neighboring_on_ : ∀ {A bounds} → (A → Set) → Coords bounds → Board A bounds → Set
 P Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] P (lookup (proj₁ neighbor) grid)
@@ -45,8 +45,8 @@ lookup∘update : ∀ {A bounds} (coords : Coords bounds) (grid : Board A bounds
 lookup∘update (x , y) grid value = begin
   lookup (x , y) (grid [ x , y ]≔ value)
     ≡⟨⟩
-  Vec.lookup x (Vec.lookup y (grid Vec.[ y ]≔ (Vec.lookup y grid Vec.[ x ]≔ value)))
-    ≡⟨ cong (Vec.lookup x) (VecProp.lookup∘update y grid (Vec.lookup y grid Vec.[ x ]≔ value)) ⟩
+  Vec.lookup x (Vec.lookup y (Vec.updateAt y (Vec._[ x ]≔ value) grid))
+    ≡⟨ cong (Vec.lookup x) (VecProp.lookup∘updateAt y grid) ⟩
   Vec.lookup x (Vec.lookup y grid Vec.[ x ]≔ value)
     ≡⟨ VecProp.lookup∘update x (Vec.lookup y grid) value ⟩
   value ∎
@@ -54,10 +54,10 @@ lookup∘update (x , y) grid value = begin
 lookup∘update′ : ∀ {A bounds} {coords₁ coords₂ : Coords bounds} → coords₁ ≢ coords₂ → ∀ (grid : Board A bounds) value →
   lookup coords₁ (grid [ coords₂ ]≔ value) ≡ lookup coords₁ grid
 lookup∘update′ {coords₁ = x₁ , y₁} {x₂ , y₂} coords₁≢coords₂ grid value with y₁ ≟ y₂
-... | no y₁≢y₂ = cong (Vec.lookup x₁) (VecProp.lookup∘update′ y₁≢y₂ grid (Vec.lookup y₂ grid Vec.[ x₂ ]≔ value))
+... | no y₁≢y₂ = cong (Vec.lookup x₁) (VecProp.lookup∘updateAt′ y₁ y₂ y₁≢y₂ grid)
 ... | yes refl = begin
   lookup (x₁ , y₁) (grid [ x₂ , y₁ ]≔ value)
-    ≡⟨ cong (Vec.lookup x₁) (VecProp.lookup∘update y₁ grid (Vec.lookup y₁ grid Vec.[ x₂ ]≔ value)) ⟩
+    ≡⟨ cong (Vec.lookup x₁) (VecProp.lookup∘updateAt y₁ grid) ⟩
   Vec.lookup x₁ (Vec.lookup y₁ grid Vec.[ x₂ ]≔ value)
     ≡⟨ VecProp.lookup∘update′ (coords₁≢coords₂ ∘ flip (curry ≡×≡⇒≡) refl) (Vec.lookup y₁ grid) value ⟩
   Vec.lookup x₁ (Vec.lookup y₁ grid) ∎
diff --git a/Minesweeper/Coords.agda b/Minesweeper/Coords.agda
index ae64181..25a262c 100644
--- a/Minesweeper/Coords.agda
+++ b/Minesweeper/Coords.agda
@@ -8,6 +8,7 @@ open import Data.Product.Relation.Pointwise.NonDependent using (≡?×≡?⇒≡
 open import Data.Fin renaming (_≟_ to _Fin≟_)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.WithK
 
 open import Minesweeper.Enumeration as Enum using (Enumeration)
 
@@ -27,7 +28,7 @@ Neighbor : ∀ {bounds} (coords : Coords bounds) → Set
 Neighbor coords = Σ[ neighbor ∈ _ ] Adjacent coords neighbor
 
 neighbors : ∀ {bounds} (coords : Coords bounds) → Enumeration (Neighbor coords)
-neighbors {w , h} coords = Enum.filter ≡-irrelevance (adjacent? coords) (Enum.allFin w Enum.⊗ Enum.allFin h)
+neighbors {w , h} coords = Enum.filter ≡-irrelevant (adjacent? coords) (Enum.allFin w Enum.⊗ Enum.allFin h)
 
 
 Adjacent-sym : ∀ {bounds} (coords₁ coords₂ : Coords bounds) → Adjacent coords₁ coords₂ → Adjacent coords₂ coords₁
diff --git a/Minesweeper/Enumeration.agda b/Minesweeper/Enumeration.agda
index 594b406..516f6ed 100644
--- a/Minesweeper/Enumeration.agda
+++ b/Minesweeper/Enumeration.agda
@@ -24,6 +24,7 @@ import Relation.Nullary.Decidable as Decidable
 open import Relation.Unary  using () renaming (Decidable to Decidable₁ ; Irrelevant to Irrelevant₁)
 open import Relation.Binary using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.WithK
 open import Data.Product using (Σ; ∃; _×_; _,_)
 open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Category.Monad
@@ -320,11 +321,11 @@ length-partition P-irrelevant Q-irrelevant which? PQ-disjoint enum = length-Σfi
 map : ∀ {A B : Set} (f : A ↔ B) → Enumeration A → Enumeration B
 map f enum = record
   { list = List.map (Inverse.to f ⟨$⟩_) (list enum)
-  ; complete = λ b → subst (_∈ List.map (Inverse.to f ⟨$⟩_) (list enum)) (Inverse.right-inverse-of f b) (∈Prop.∈-map⁺ (complete enum (Inverse.from f ⟨$⟩ b)))
-  ; entries-unique = λ ix₁ ix₂ → Inverse.injective (Inverse.sym ∈Prop.map-∈↔) (images-unique (Inverse.from ∈Prop.map-∈↔ ⟨$⟩ ix₁) (Inverse.from ∈Prop.map-∈↔ ⟨$⟩ ix₂)) } where
+  ; complete = λ b → subst (_∈ List.map (Inverse.to f ⟨$⟩_) (list enum)) (Inverse.right-inverse-of f b) (∈Prop.∈-map⁺ _ (complete enum (Inverse.from f ⟨$⟩ b)))
+  ; entries-unique = λ ix₁ ix₂ → Inverse.injective (Inverse.sym (∈Prop.map-∈↔ _)) (images-unique (Inverse.from (∈Prop.map-∈↔ _) ⟨$⟩ ix₁) (Inverse.from (∈Prop.map-∈↔ _) ⟨$⟩ ix₂)) } where
     images-unique : ∀ {b} (ix₁ ix₂ : ∃ λ a → a ∈ list enum × b ≡ Inverse.to f ⟨$⟩ a) → ix₁ ≡ ix₂
     images-unique (a₁ , a₁∈enum , b≡fa₁) (a₂  , a₂∈enum , b≡fa₂) with Inverse.injective f (trans (sym b≡fa₁) (b≡fa₂))
-    images-unique (a₁ , a₁∈enum , b≡fa₁) (.a₁ , a₂∈enum , b≡fa₂) | refl = cong (a₁ ,_) (cong₂ _,_ (entries-unique enum a₁∈enum a₂∈enum) (≡-irrelevance b≡fa₁ b≡fa₂))
+    images-unique (a₁ , a₁∈enum , b≡fa₁) (.a₁ , a₂∈enum , b≡fa₂) | refl = cong (a₁ ,_) (cong₂ _,_ (entries-unique enum a₁∈enum a₂∈enum) (≡-irrelevant b≡fa₁ b≡fa₂))
 
 length-map : ∀ {A B : Set} (f : A ↔ B) (enum : Enumeration A) → List.length (list (map f enum)) ≡ List.length (list enum)
 length-map f enum = ListProp.length-map (Inverse.to f ⟨$⟩_) (list enum)