rw [this]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypeColumn ((fst✝, snd✝) :: ss) pf τ) = names ((fst✝, snd✝) :: ss)