intro eqt
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
⊢ hasNameEqHeadOrTail h ≡ Sum.inl (EqT.refl nm) → h = HasName.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
eqt : hasNameEqHeadOrTail h ≡ Sum.inl (EqT.refl nm)
⊢ h = HasName.hd