simp only [List.mem_append, or_assoc, not_or]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ++ Board.pathB n i ++ Board.pathR m j ++ Board.pathT i j
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ∧
    ¬Board.pivot i j ∈ Board.pathB n i ∧ ¬Board.pivot i j ∈ Board.pathR m j ∧ ¬Board.pivot i j ∈ Board.pathT i j