cases eqt
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt : Sum.inr a✝ ≡ Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
case tl.refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl : HasName nm hs
⊢ HasName.tl htl = HasName.tl htl