-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
          rev
          (Γ'.bit1 ::
            update (β := fun (k : K') ↦ List Γ') (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?.getD default) then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
      else
        TM2.stepAux (Γ := fun (x : K') ↦ Γ')
          (peek' main
            (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
              (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
have h : elim (Γ'.cons :: trList v) [] c d =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ')
      ((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂))
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
              (update (β := fun (k : K') ↦ List Γ')
                (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                rev
                (Γ'.bit1 ::
                  update (β := fun (k : K') ↦ List Γ') (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?.getD default) then
              TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
            else
              TM2.stepAux (Γ := fun (x : K') ↦ Γ')
                (peek' main
                  (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                    (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                    (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                      (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
        (Γ := fun (x : K') ↦ Γ'))
      rev [])
    main
    (((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
              TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ')
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                  rev
                  (Γ'.bit1 ::
                    update (β := fun (k : K') ↦ List Γ') (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?.getD default) then
                TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
              else
                TM2.stepAux (Γ := fun (x : K') ↦ Γ')
                  (peek' main
                    (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                      (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                      (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
          (Γ := fun (x : K') ↦ Γ') rev).reverseAux
      ((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂))
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
              (update (β := fun (k : K') ↦ List Γ')
                (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                rev
                (Γ'.bit1 ::
                  update (β := fun (k : K') ↦ List Γ') (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?.getD default) then
              TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
            else
              TM2.stepAux (Γ := fun (x : K') ↦ Γ')
                (peek' main
                  (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                    (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                    (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                      (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
        (Γ := fun (x : K') ↦ Γ') main))
Tactic: convert! unrev_ok using 2