cases sch with
| nil => contradiction
| cons s ss => simp [hasNameOfFromCHeaders]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
τ : Type u_1
hpf : HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
no goals