simp only [hasNameEqHeadOrTail] at eqt
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
eqt : hasNameEqHeadOrTail h ≡ Sum.inr htl
⊢ h = HasName.tl htl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
eqt :
  (match nm, hs, h with
    | .(h✝.fst), x, HasName.hd => Sum.inl (EqT.refl h✝.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ h = HasName.tl htl