∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp k.cons₂ =
    Turing.PartrecToTM2.trStmts₁
        (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪
      Turing.PartrecToTM2.contSupp k