∀ {α : Type u} {β : Type v} (f : α → Computation β) (ca : Computation α),
  Computation.Bind.f f (Sum.inl ca) =
    match ca.destruct with
    | Sum.inl a => Computation.Bind.g (f a).destruct
    | Sum.inr ca' => Sum.inr (Sum.inl ca')