fix up inductive definition of valid moves

oops! I'd forgotten a condition and the old definition was too weak.
when making an "a tile already has as many neighboring mines as it can, so its
other neighbors are safe" statement, the list of neighboring mines provided as
evidence must have unique elements!

Minesweeper/Reasoning.agda

@@ -8,6 +8,7 @@ open import Relation.Binary.PropositionalEquality
 open import Data.List as List using (List)
 open import Data.List.Membership.Propositional
 open import Data.Product
+open import Data.List.All as All using (All; []; _∷_)
 open import Data.Nat
 
 open import Data.Fin using (Fin)
@@ -20,7 +21,18 @@ open import Minesweeper.Moves
 -- our inductive family for minesweeper proofs! based on ProofSweeper but using our own machinery
 -- and not intended for hand-writing at all
 data _[_]↝★_ {bounds} (grid : Board Tile bounds) (coords : Coords bounds) : Guess → Set
-record _Neighboring★_on_excluding_ {bounds} (guess : Guess) (neighbor : Coords bounds) (grid : Board Tile bounds) (exclusion : Coords bounds) : Set
+record Neighbors★ {bounds} (grid : Board Tile bounds) (neighbor : Coords bounds) (exclude : Coords bounds) (guess : Guess) : Set
+Many_neighboring★_on_excluding_ : ∀ {bounds} → Guess → Coords bounds → Board Tile bounds → Coords bounds → Set
+
+record Neighbors★ {bounds} grid neighbor exclude guess where
+  inductive
+  field
+    list : List (Neighbor neighbor)
+    unique : ∀ {elem} (ix₁ ix₂ : elem ∈ list) → ix₁ ≡ ix₂
+    guess-valid★ : All (λ elem → grid [ proj₁ elem ]↝★ guess) list
+    exclusion : All (λ elem → exclude ≢ proj₁ elem) list
+
+Many_neighboring★_on_excluding_ guess neighbor grid exclude = Neighbors★ grid neighbor exclude guess
 
 data _[_]↝★_ {bounds} grid coords where
   -- known tiles already have a proven identity
@@ -29,20 +41,14 @@ data _[_]↝★_ {bounds} grid coords where
   -- a tile is safe if an adjacent safe tile already has as many adjacent mines as it can
   safe★ : ∀ neighborMineCount
     (safeNeighbor : known (safe neighborMineCount) Neighboring coords on grid)
-    (neighborMines : List (mine⚐ Neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords)) →
-    List.length neighborMines ≡ neighborMineCount →
+    (neighborMines : Many mine⚐ neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords) →
+    List.length (Neighbors★.list neighborMines) ≡ neighborMineCount →
       grid [ coords ]↝★ safe⚐
 
   -- a tile is a mine if an adjacent safe tile already has as many adjacent safe tiles as it can
   mine★ : ∀ neighborMineCount
     (safeNeighbor : known (safe neighborMineCount) Neighboring coords on grid)
-    (neighborSafes : List (safe⚐ Neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords)) →
-    List.length neighborSafes + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeNeighbor)))) →
+    (neighborSafes : Many safe⚐ neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords) →
+    List.length (Neighbors★.list neighborSafes) + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeNeighbor)))) →
       grid [ coords ]↝★ mine⚐
 
-record _Neighboring★_on_excluding_ {bounds} guess neighbor grid exclusion where
-  inductive
-  field
-    coords : Coords bounds
-    deduction : grid [ coords ]↝★ guess
-    ≢exclusion : coords ≢ exclusion