simp only [List.filter, List.notElem, List.elem]
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names ((nm, τ) :: s'))
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')