∀ (motive : (_ : ℕ) ×' ℕ → Prop),
  (∀ (n : ℕ), motive ⟨0, n⟩) →
    (∀ (m : ℕ), motive ⟨m, 1⟩ → motive ⟨m.succ, 0⟩) →
      (∀ (m n : ℕ), motive ⟨m + 1, n⟩ → motive ⟨m, ack._unary ⟨m + 1, n⟩⟩ → motive ⟨m.succ, n.succ⟩) →
        ∀ (_x : (_ : ℕ) ×' ℕ), motive _x