cases heqt
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
heqt : (nth sch n (_ : Nat.succ n ≤ length sch)).fst ≡ nm
h : hasNameEqHeadOrTail hnths = Sum.inl heqt
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hnths }
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hnths } =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName hnths }