∀ {α : Type u_2} {β : Type u_1} {p : α ⊕ β → Prop},
  Function.RightInverse
    (fun x =>
      match x with
      | Sum.inl a => ⟨Sum.inl ↑a, ⋯⟩
      | Sum.inr b => ⟨Sum.inr ↑b, ⋯⟩)
    fun x =>
    match x with
    | ⟨Sum.inl a, h⟩ => Sum.inl ⟨a, h⟩
    | ⟨Sum.inr b, h⟩ => Sum.inr ⟨b, h⟩