∀ {α : Type u_1} (motive : WithBot α → WithBot α → Prop) (a b : WithBot α),
  (∀ (a : Unit), motive none none) →
    (∀ (b : α), motive none (some b)) →
      (∀ (a : α), motive (some a) none) → (∀ (a b : α), motive (some a) (some b)) → motive a b