apply ih
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ