Theorem: list_cons_to_set_union (FOL/Parsing/DFT.lean)

State before:
α : Type
inst : DecidableEq α
ys : List α
x : α
⊢ ↑(x :: ys).toFinset = {x} ∪ ↑ys.toFinset
Tactic:
ext a
State after:
case h
α : Type
inst : DecidableEq α
ys : List α
x a : α
⊢ a ∈ ↑(x :: ys).toFinset ↔ a ∈ {x} ∪ ↑ys.toFinset

State before:
case h
α : Type
inst : DecidableEq α
ys : List α
x a : α
⊢ a ∈ ↑(x :: ys).toFinset ↔ a ∈ {x} ∪ ↑ys.toFinset
Tactic:
simp
State after:
no goals