simp only [lookupType]
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h } =
    (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd