simp only [Schema.lookupType]
η : 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)))
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := 0, isLt := hlt } :: ns)) { fst := snm, snd := HasName.hd } =
    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 := hasNameOfNthsHasName HasName.hd }