simp only [Schema.fromCHeaders, List.map, List.append, Schema.hasNameOfAppend]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.fromCHeaders ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := { fst := nm, snd := Schema.HasName.hd }.fst,
        snd := Schema.hasNameOfAppend { fst := nm, snd := Schema.HasName.hd }.snd } =
    Schema.lookup sch
      { fst := { fst := nm, snd := Schema.HasName.hd }.fst,
        snd := Schema.hasNameOfFromCHeaders { fst := nm, snd := Schema.HasName.hd }.snd }
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.hd } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders Schema.HasName.hd }