∀ {V : Type u_1} {v : V} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] {s : Finset V}
  [inst_2 : DecidableRel G.Adj], v ∈ s → G.neighborFinset v ⊆ (SimpleGraph.between (↑s) (↑s)ᶜ G).neighborFinset v ∪ s