. contradiction
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
hs : List Header
htl : HasName nm hs
τ✝ : Type u_2
eqt :
  (match nm, hs, HasName.hd with
    | .((nm, τ✝).fst), x, HasName.hd => Sum.inl (EqT.refl (nm, τ✝).fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.hd = HasName.tl htl

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