c : Code
h : Ok c
v : List ℕ
⊢ (do
      let v ← eval c v
      Turing.eval step (Cfg.ret Cont.halt v)) =
    do
    let a ← eval c v
    pure (Cfg.halt a)
c : Code
h : Ok c
v : List ℕ
⊢ Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> eval c v
rw [h, ← bind_pure_comp]
case e_a
c : Code
h : Ok c
v : List ℕ
⊢ (fun v => Turing.eval step (Cfg.ret Cont.halt v)) = fun a => pure (Cfg.halt a)
c : Code
h : Ok c
v : List ℕ
⊢ (do
      let v ← eval c v
      Turing.eval step (Cfg.ret Cont.halt v)) =
    do
    let a ← eval c v
    pure (Cfg.halt a)
congr
case e_a.h
c : Code
h : Ok c
v✝ v : List ℕ
⊢ Turing.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)
case e_a
c : Code
h : Ok c
v : List ℕ
⊢ (fun v => Turing.eval step (Cfg.ret Cont.halt v)) = fun a => pure (Cfg.halt a)
funext v
no goals
case e_a.h
c : Code
h : Ok c
v✝ v : List ℕ
⊢ Turing.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)