∀ {α : Type u_1} {β : Sort u_2} {o o' : Option α} {b b' : β} {f : (a : α) → o = some a → β}
  {g : (a : α) → o' = some a → β} (ho : o = o'),
  b = b' → (∀ (a : α) (ha : o' = some a), f a ⋯ = g a ha) → o.pelim b f = o'.pelim b' g