apply lookup_of_colImpliesName
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup ss { fst := nm, snd := colImpliesName h } = (nm, τ)
no goals