Halts With Result iff eval

theorem haltsWithResult_iff_eval {inputs : List ℕ} {result : ℕ} :    p ↓ inputs ≫ result ↔ eval p inputs = Part.some result := by  rw [Part.eq_some_iff, eval, Part.mem_map_iff]  constructor  · intro ⟨s, hsteps, hhalted, hresult⟩    have hhalts : Halts p inputs := ⟨s, hsteps, hhalted⟩    have heq : (evalState p inputs).get hhalts = s :=      Steps.eq_of_halts (evalState_spec p hhalts).1 (evalState_spec p hhalts).2 hsteps hhalted    exact ⟨(evalState p inputs).get hhalts, Part.get_mem hhalts, heq ▸ hresult⟩  · intro ⟨s, hs_mem, hresult⟩    rw [Part.mem_eq] at hs_mem    obtain ⟨hdom, hget⟩ := hs_mem    have hspec := evalState_spec p hdom    exact ⟨s, hget ▸ hspec.1, hget ▸ hspec.2, hresult⟩