cases h with
| inl h => exact h ▸ hv
| inr h => exact h ▸ hw
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v ∨ x = w
⊢ x ∈ A
no goals