∀ {α : Type u_2} {β : Type u_1} (R : α → β → Prop) (a : α) (cb : Computation β) (motive : (∃ b ∈ cb, R a b) → Prop)
  (x : ∃ b ∈ cb, R a b), (∀ (b : β) (mb : b ∈ cb) (ab : R a b), motive ⋯) → motive x