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