simp only [Schema.fromCHeaders, List.map, List.append, Schema.hasNameOfAppend]
η : 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.fromCHeaders ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := { fst := nm, snd := Schema.HasName.tl a✝ }.fst,
        snd := Schema.hasNameOfAppend { fst := nm, snd := Schema.HasName.tl a✝ }.snd } =
    Schema.lookup sch
      { fst := { fst := nm, snd := Schema.HasName.tl a✝ }.fst,
        snd := Schema.hasNameOfFromCHeaders { fst := nm, snd := Schema.HasName.tl a✝ }.snd }
η : 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 ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.tl (Schema.hasNameOfAppend a✝) } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders (Schema.HasName.tl a✝) }