∀ (motive : ℤ → ℤ → Prop) (x x_1 : ℤ),
  (∀ (m : ℕ), motive (Int.ofNat m) 0) →
    (∀ (a a_1 : ℕ), motive (Int.ofNat a) (Int.negSucc a_1)) →
      (∀ (a n : ℕ), motive (Int.negSucc a) (Int.ofNat n.succ)) →
        (∀ (a n : ℕ), motive (Int.ofNat a) (Int.ofNat n.succ)) →
          (∀ (a : ℕ), motive (Int.negSucc a) 0) →
            (∀ (a a_1 : ℕ), motive (Int.negSucc a) (Int.negSucc a_1)) → motive x x_1