∀ {V : Type u_1} {α : Type u_2} {β : Type u_3} (left : Finset V) (this : Nonempty (α ↪ ↥left)) {s₁ : α ⊕ β}
  (hs₁ : s₁.isLeft = true), (Subtype.val ∘ ⇑(Classical.arbitrary (α ↪ ↥left))) (s₁.getLeft hs₁) ∈ ↑left