unfold Schema.hasNameOfNthsHasName
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ sτ = lookupType ((snm, sτ) :: sch) { fst := snm, snd := hasNameOfNthsHasName HasName.hd }
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ sτ =
    lookupType ((snm, sτ) :: sch)
      { fst := snm,
        snd :=
          match snm, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := 0, isLt := hlt }.val
                  (_ : { val := 0, isLt := hlt }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := 0, isLt := hlt }.val
                      (_ : { val := 0, isLt := hlt }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := 0, isLt := hlt }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }