{α : Type u_1} →
  (motive : WithZero α → ℤ → Sort u_2) →
    (x : WithZero α) →
      (x_1 : ℤ) →
        (Unit → motive none (Int.ofNat 0)) →
          ((n : ℕ) → motive none (Int.ofNat n.succ)) →
            ((a : ℕ) → motive none (Int.negSucc a)) → ((x : α) → (n : ℤ) → motive (some x) n) → motive x x_1