-- Mathlib/Computability/TMToPartrec.lean
theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s',
    Reaches₁ (TM2.step tr) ⟨some (Λ'.pred q₁ q₂), s, K'.elim (trList v) [] c d⟩
      (v.headI.rec ⟨some q₁, s', K'.elim (trList v.tail) [] c d⟩ fun n _ =>
        ⟨some q₂, s', K'.elim (trList (n::v.tail)) [] c d⟩)

Proof state:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
refine TransGen.head rfl ?_

Result:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (tr (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Proof state:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
      { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
        stk :=
          update
            (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
            rev
            (Γ'.bit1 ::
              update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev) }
    else
      bif natEnd (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.iget then
        { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
          stk :=
            update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
      else
        TM2.stepAux
          (peek' main
            (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
              (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂))))
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
convert unrev_ok using 2

Result:
case h.e'_2.h.e'_7
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ elim (Γ'.cons :: trList v) [] c d =
    update
      (update
        (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
            { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
              stk :=
                update
                  (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                  rev
                  (Γ'.bit1 ::
                    update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev) }
          else
            bif natEnd (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.iget then
              { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                stk :=
                  update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
            else
              TM2.stepAux
                (peek' main
                  (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
                    (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂))))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
        rev [])
      main
      (((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
                { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                  stk :=
                    update
                      (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                      rev
                      (Γ'.bit1 ::
                        update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev) }
              else
                bif natEnd (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.iget then
                  { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                    stk :=
                      update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
                else
                  TM2.stepAux
                    (peek' main
                      (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
                        (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂))))
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                    (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
            rev).reverseAux
        ((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
              { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                stk :=
                  update
                    (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                    rev
                    (Γ'.bit1 ::
                      update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev) }
            else
              bif natEnd (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.iget then
                { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                  stk :=
                    update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
              else
                TM2.stepAux
                  (peek' main
                    (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
                      (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂))))
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
          main))