rw [Schema.lookup_eq_2, Schema.lookup_eq_2]
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := HasName.tl (hasNameOfAppend h') }
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }