∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : { e // e none = x }),
  (fun e =>
        ⟨{ toFun := fun a => a.casesOn' x (Subtype.val ∘ ⇑e),
            invFun := fun b => if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
          ⋯⟩)
      ((fun e =>
          { toFun := fun a => ⟨↑e (some a), ⋯⟩, invFun := fun b => ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
            right_inv := ⋯ })
        e) =
    e