apply pivotTable_spec3_aux cs aggs ⟨nm, _⟩
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup (Schema.append (Schema.map Sigma.fst cs) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.hasNameOfAppend a✝ } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders a✝ }
no goals