Steps to Standard Form halts

theorem Steps.toStandardForm_halts {p : Program} {s s' : State}    (hsteps : Steps p s s') (hhalted : s'.isHalted p) :    ∃ s₂, Steps p.toStandardForm s s₂ ∧      s₂.isHalted p.toStandardForm ∧ s'.regs = s₂.regs := by  induction hsteps using Relation.ReflTransGen.head_induction_on with  | refl =>    refine ⟨s', .refl, ?_, rfl⟩    simp only [State.isHalted, Program.toStandardForm_length]    exact hhalted  | head hstep hrest ih =>    rcases Step.toStandardForm hstep with      hsame | ⟨hhalted_mid, s_mid, hstep_mid, hhalted_mid', hregs_eq⟩    · obtain ⟨s₂, hsteps₂, hhalted₂, hregs_eq⟩ := ih      exact ⟨s₂, .trans (.single hsame) hsteps₂, hhalted₂, hregs_eq⟩    · grind [Steps.eq_of_halts .refl hhalted_mid hrest hhalted]