induction pf with
| hd =>
  simp only [lookupType]
  rw [lookup_eq_1]
| tl h ih =>
  simp only [lookupType]
  rw [lookup_eq_2]
  apply ih
case mk
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
pf : HasName nm s
⊢ lookupType s { fst := nm, snd := pf } = (lookup s { fst := nm, snd := pf }).snd
no goals