simp [hasNameOfFromCHeaders]
case cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
s : Header
ss : List Header
hpf : HasCol (nm, τ) (s :: ss)
cs : List (CertifiedHeader (s :: ss))
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
no goals