case nil
α : Type u_1
β : Type ?u.470224
γ : Type ?u.470227
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset ([] ++ l') = toFinset [] ∪ toFinset l'

case cons
α : Type u_1
β : Type ?u.470224
γ : Type ?u.470227
inst✝ : DecidableEq α
l l' : List α
a hd : α
tl : List α
hl : toFinset (tl ++ l') = toFinset tl ∪ toFinset l'
⊢ toFinset (hd :: tl ++ l') = toFinset (hd :: tl) ∪ toFinset l'
α : Type u_1
β : Type ?u.470224
γ : Type ?u.470227
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset (l ++ l') = toFinset l ∪ toFinset l'
induction' l with hd tl hl
no goals
case nil
α : Type u_1
β : Type ?u.470224
γ : Type ?u.470227
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset ([] ++ l') = toFinset [] ∪ toFinset l'
simp
no goals
case cons
α : Type u_1
β : Type ?u.470224
γ : Type ?u.470227
inst✝ : DecidableEq α
l l' : List α
a hd : α
tl : List α
hl : toFinset (tl ++ l') = toFinset tl ∪ toFinset l'
⊢ toFinset (hd :: tl ++ l') = toFinset (hd :: tl) ∪ toFinset l'
simp [hl]