Steps from to Standard Form halts

theorem Steps.from_toStandardForm_halts {p : Program} {s s' : State}    (hsteps : Steps p.toStandardForm s s') (hhalted : s'.isHalted p.toStandardForm) :    ∃ s₂, Steps p s s₂ ∧ s₂.isHalted p ∧ s'.regs = s₂.regs := by  induction hsteps using Relation.ReflTransGen.head_induction_on with  | refl =>    refine ⟨s', by rfl, ?_, rfl⟩    simp only [State.isHalted, Program.toStandardForm_length] at hhalted ⊢    exact hhalted  | head hstep hrest ih =>    rcases Step.from_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⟩    · rename_i s_next      have hrest_trivial : s_next = s' := Steps.eq_of_halts .refl hhalted_mid hrest hhalted      subst hrest_trivial      exact ⟨s_mid, .single hstep_mid, hhalted_mid', hregs_eq⟩