∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  (∀ a ∈ ca, Computation.LiftRel R ca cb) → (∀ b ∈ cb, Computation.LiftRel R ca cb) → Computation.LiftRel R ca cb