simp only [Schema.lookupType]
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
t : Table []
f : Row [] → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead [] c τ []) } =
    τ
no goals