intros s t c h
η : 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 }
η : 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 }