induction hc with
| @hd nm s' τ =>
  simp only [List.filter, List.notElem, List.elem]
  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
| @tl hdr nm s' h ih =>
  simp only [Schema.names, List.map]
  cases hdr with | mk nm₁ τ₁ =>
  cases Decidable.em (nm₁ = nm) with
  | inl heq =>
    rw [heq] at hsch
    cases hsch with | cons hnmem hu =>
    simp only at hnmem
    have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
    contradiction
  | inr hneq =>
    rw [←List.removeAllEq]
    rw [List.removeAllEq_singleton_hd_neq]
    . congr
      apply ih
      . cases hsch; assumption
      . exact Table.mk []
    . exact hneq
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : List.Unique (Schema.names sch)
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
no goals