simp only [Schema.names, List.map]
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ Schema.names (Schema.removeName (hdr :: s') (Schema.HasName.tl h)) =
    List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names (hdr :: s'))
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ hdr.fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) (hdr.fst :: List.map Prod.fst s')