conv =>
  rhs
  unfold Schema.hasNameOfNthsHasName
  simp only [Schema.hasNameEqHeadOrTail]
η : 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)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName (HasName.tl h) }
η : 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)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName h }