∀ {α : Type u_1} {β : Type u_2} (motive : Computation α ⊕ Computation β → Sort u_3) (ca : Computation α)
  (h_1 : (ca : Computation α) → motive (Sum.inl ca)) (h_2 : (cb : Computation β) → motive (Sum.inr cb)),
  (match Sum.inl ca with
    | Sum.inl ca => h_1 ca
    | Sum.inr cb => h_2 cb) =
    h_1 ca