∀ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) (a : α) (cb : Computation β)
  (motive : Computation.LiftRel R (Computation.pure a) cb → Prop) (x : Computation.LiftRel R (Computation.pure a) cb),
  (∀ (l : ∀ {a_1 : α}, a_1 ∈ Computation.pure a → ∃ b ∈ cb, R a_1 b)
      (right : ∀ {b : β}, b ∈ cb → ∃ a_2 ∈ Computation.pure a, R a_2 b), motive ⋯) →
    motive x