simp only [hasNameOfFromCHeaders_eq_1]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := hasNameOfFromCHeaders HasName.hd } = ch_τ
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := colImpliesName (HasCol.tl h) } = ch_τ