-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ TM2.step (Γ := fun (x : K') ↦ Γ') tr a = some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
have h : Eq (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
    (update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
              (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
            main
            ((fun (x : Option Γ') ↦ Γ'.cons)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
          main
          ((fun (x : Option Γ') ↦ Γ'.bit1)
              ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
            update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
              main))
        rev [])
      main
      ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
            main
            ((fun (x : Option Γ') ↦ Γ'.bit1)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                main)
            rev).reverseAux
        (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
              (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
            main
            ((fun (x : Option Γ') ↦ Γ'.cons)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
          main
          ((fun (x : Option Γ') ↦ Γ'.bit1)
              ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
            update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
              main)
          main))))
Tactic: convert! unrev_ok using 1