∀ (motive : ZNum → Sort u_1) (a : PosNum) (h_1 : Unit → motive ZNum.zero) (h_2 : (a : PosNum) → motive (ZNum.pos a))
  (h_3 : (a : PosNum) → motive (ZNum.neg a)),
  (match ZNum.neg a with
    | ZNum.zero => h_1 ()
    | ZNum.pos a => h_2 a
    | ZNum.neg a => h_3 a) =
    h_3 a