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