simp only [List.map]
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ List.map Prod.fst (Schema.append (s :: ss) [(c, τ)]) = List.map Prod.fst (s :: ss) ++ [c]
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ s.fst :: List.map Prod.fst (Schema.append ss [(c, τ)]) = s.fst :: List.map Prod.fst ss ++ [c]