intro t cs inst 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))),
    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))
⊢ header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)