induction h with
| hd =>
  simp only [Schema.hasNameOfAppend]
  rw [Schema.lookup_eq_1, Schema.lookup_eq_1]
| tl h' ih =>
  simp only [Schema.hasNameOfAppend]
  rw [Schema.lookup_eq_2, Schema.lookup_eq_2]
  exact ih
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
h : HasName c s
⊢ lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }
no goals