cases hsch with | cons hnmem hu =>
simp only at hnmem
have : (decide (nm ∉ [nm])) = false :=
  by simp only [decide_not, List.mem_singleton_iff, decide_True,
                decide_False, not]
rw [this]
simp only
simp only [Schema.names, List.map]
have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
        = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
rw [this]
rw [List.removeAllEq_singleton_nonelem_eq]
exact hnmem
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')
no goals