unfold Schema.hasNameOfNthsHasName
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)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName HasName.hd }
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)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd :=
          match (nth sch n (_ : Nat.succ n ≤ length sch)).fst, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                  (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                      (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := Nat.succ n, isLt := pf }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }