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