-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
case :
  ∀
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
          (elim (trList v) [] [] (trContStack k)))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
            (elim (trList v.tail) [] [] (trContStack k)))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
              (elim (trList (n :: v.tail)) [] [] (trContStack k)))
          0)),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∀
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
          (elim (trList v) [] [] (trContStack k)))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
            (elim (trList v.tail) [] [] (trContStack k)))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
              (elim (trList (n :: v.tail)) [] [] (trContStack k)))
          v.headI)),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
have case₁ : ∀ (n : ℕ)
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
        (elim (trList v) [] [] (trContStack k)))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
          (elim (trList v.tail) [] [] (trContStack k)))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
            (elim (trList (n :: v.tail)) [] [] (trContStack k)))
        (n + 1))),
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
Tactic: rcases v.headI with - | n