diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda
index 75dcc31..c5a1d07 100644
--- a/Minesweeper/Board.agda
+++ b/Minesweeper/Board.agda
@@ -2,8 +2,8 @@ module Minesweeper.Board where
 
 open import Data.Vec as Vec using (Vec)
 import Data.Vec.Properties as VecProp
-import Data.Vec.Relation.Pointwise.Inductive   as VecIndPointwise
-import Data.Vec.Relation.Pointwise.Extensional as VecExtPointwise
+import Data.Vec.Relation.Binary.Pointwise.Inductive   as VecIndPointwise
+import Data.Vec.Relation.Binary.Pointwise.Extensional as VecExtPointwise
 open import Data.Fin using (_≟_)
 open import Data.Product
 open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡)
diff --git a/Minesweeper/Enumeration.agda b/Minesweeper/Enumeration.agda
index 516f6ed..7d9b5dc 100644
--- a/Minesweeper/Enumeration.agda
+++ b/Minesweeper/Enumeration.agda
@@ -3,7 +3,7 @@ module Minesweeper.Enumeration where
 open import Data.List as List using (List; []; _∷_)
 import Data.List.Categorical as List
 import Data.List.Properties as ListProp
-open import Data.List.Any as Any using (Any ; here ; there)
+open import Data.List.Relation.Unary.Any as Any using (Any ; here ; there)
 import Data.List.Any.Properties as AnyProp
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Propositional.Properties as ∈Prop
diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda
index bd93d82..c83ada3 100644
--- a/Minesweeper/Moves.agda
+++ b/Minesweeper/Moves.agda
@@ -6,9 +6,9 @@ open import Data.Empty
 open import Data.Product
 open import Data.Sum
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
-open import Data.Vec.Relation.Pointwise.Inductive as VecPointwise using ([]; _∷_)
-open import Data.Vec.Any as Any using (Any; any)
-import      Data.Vec.Any.Properties as AnyProp
+open import Data.Vec.Relation.Unary.Any as Any using (Any; any)
+import      Data.Vec.Relation.Unary.Any.Properties as AnyProp
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as VecPointwise using ([]; _∷_)
 open import Data.Vec.Membership.Propositional using (_∈_)
 import      Data.Vec.Membership.Propositional.Properties as ∈
 open import Data.Nat hiding (_>_; _≥_)
diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda
index 3e37467..a9af769 100644
--- a/Minesweeper/Reasoning.agda
+++ b/Minesweeper/Reasoning.agda
@@ -7,12 +7,12 @@ open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
 open import Data.Empty
 open import Data.List as List using (List; []; _∷_)
-open import Data.List.Relation.Pointwise as Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties using (there-injective)
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Membership.Propositional
-open import Data.List.All as All using (All; []; _∷_)
-open import Data.List.All.Properties using (All¬⇒¬Any)
-open import Data.List.Any as Any using (Any; here; there)
-open import Data.List.Any.Properties using (there-injective)
 open import Data.Product as Σ
 open import Data.Product.Properties
 open import Data.Nat