∀ (α β : Type u_1) (s : α ⊕ β),
  (fun s =>
        match s with
        | ⟨false, a⟩ => Sum.inl a
        | ⟨true, b⟩ => Sum.inr b)
      ((fun s => Sum.elim (fun x => ⟨false, x⟩) (fun x => ⟨true, x⟩) s) s) =
    s