simp only [List.mem_pmap, not_exists]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin ((m + 1) * (n + 1))) (x_1 : ↑x < (m + 1) * (n + 1) - 1),
    ¬(x ∈ Board.path i j ∧
        Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict x x_1)