rw [Schema.lookup_eq_1, Schema.lookup_eq_1]
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := HasName.hd }
no goals