Eq of halts

theorem eq_of_halts {init s₁ s₂ : State}    (h1 : Steps p init s₁) (hh1 : s₁.isHalted p)    (h2 : Steps p init s₂) (hh2 : s₂.isHalted p) : s₁ = s₂ := by  -- Use confluence: both s₁ and s₂ are reachable from init, so they're joinable  have ⟨w, hw1, hw2⟩ := step_confluent p h1 h2  -- But s₁ and s₂ are normal forms, so w must equal both  have hn1 := isHalted_iff_normal.mp hh1  have hn2 := isHalted_iff_normal.mp hh2  obtain ⟨pc₁, regs₁⟩ := s₁  obtain ⟨pc₂, regs₂⟩ := s₂  grind