(motive : ℕ → Sort u_1) →
  (x : ℕ) →
    (Unit → motive 0) →
      (Unit → motive 1) →
        (Unit → motive 2) → ((x : ℕ) → (x = 0 → False) → (x = 1 → False) → (x = 2 → False) → motive x) → motive x