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