have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
        = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')