∀ (motive : Num → Num → Prop) (x x_1 : Num),
  (∀ (a : Unit), motive Num.zero Num.zero) →
    (∀ (_a : PosNum), motive (Num.pos _a) Num.zero) →
      (∀ (_b : PosNum), motive Num.zero (Num.pos _b)) →
        (∀ (_a _b : PosNum), motive (Num.pos _a) (Num.pos _b)) → motive x x_1