∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] (x : { x // p x ∨ q x }),
  Sum.elim (⇑(Subtype.impEmbedding p (fun x => p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x => p x ∨ q x) ⋯))
      ((subtypeOrLeftEmbedding p q) x) =
    x