Eval State to Standard Form regs

theorem evalState_toStandardForm_regs {p : Program} {inputs : List ℕ}    (hp : (evalState p inputs).Dom) (hq : (evalState p.toStandardForm inputs).Dom) :    ((evalState p inputs).get hp).regs =      ((evalState p.toStandardForm inputs).get hq).regs := by  have ⟨hsteps, hhalted⟩ := evalState_spec p hp  have ⟨hsteps', hhalted'⟩ := evalState_spec p.toStandardForm hq  obtain ⟨s₂, hsteps₂, hhalted₂, hregs_eq⟩ := Steps.toStandardForm_halts hsteps hhalted  rw [Steps.eq_of_halts hsteps' hhalted' hsteps₂ hhalted₂, hregs_eq]