∀
  (motive :
    (x : Turing.ToPartrec.Cfg) →
      (x_1 : Turing.TM2.Cfg (fun x => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')) →
        Turing.PartrecToTM2.TrCfg x x_1 → Prop)
  (x : Turing.ToPartrec.Cfg)
  (x_1 : Turing.TM2.Cfg (fun x => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ'))
  (x_2 : Turing.PartrecToTM2.TrCfg x x_1),
  (∀ (a : Turing.ToPartrec.Cont) (a_1 : List ℕ) (w : Option Turing.PartrecToTM2.Γ'),
      motive (Turing.ToPartrec.Cfg.ret a a_1)
        { l := some (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.trCont a)), var := w,
          stk :=
            Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList a_1) [] [] (Turing.PartrecToTM2.trContStack a) }
        ⋯) →
    (∀ (v : List ℕ), motive (Turing.ToPartrec.Cfg.halt v) (Turing.PartrecToTM2.halt v) ⋯) → motive x x_1 x_2