intro x
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
⊢ {v, w} ⊆ A
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x ∈ {v, w} → x ∈ A