simp only [retypedFromSubschema]
η : 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))
⊢ names (retypedFromSubschema ({ fst := (nm, τ), snd := pf } :: 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))
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)