apply lookupType_nths_eq_lookupType
η : 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))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
htoprove : hnths = HasName.tl hhnm
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := hhnm } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }
no goals