rw [colImpliesName_eq_1 (sch' := ss) (hdr := (nm, τ)),
    lookup_eq_1]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
ss : List Header
⊢ lookup ((nm, τ) :: ss) { fst := nm, snd := colImpliesName HasCol.hd } = (nm, τ)
no goals