simp only [header, Schema.names, Schema.fromCHeaders,
           Schema.append_eq_List_append, Schema.map_eq_List_map]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ List.map Prod.fst (List.append (List.map Sigma.fst cs) (List.map (fun x => x.fst) aggs)) =
    List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)