generalize hv : getUnique xs h = v
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
⊢ getUnique xs h ∈ y ↔ xs ⊆ y
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : getUnique xs h = v
⊢ v ∈ y ↔ xs ⊆ y