∀ {α : Type u_1} (motive : WithZero α → WithZero α → Prop) (x x_1 : WithZero α),
  (∀ (x : WithZero α), motive none x) →
    (∀ (val : α), motive (some val) none) → (∀ (val val_1 : α), motive (some val) (some val_1)) → motive x x_1