∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }),
  (fun e =>
        { toFun := fun a => ⟨↑e (some a), ⋯⟩, invFun := fun b => ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ })
      ((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 := ⋯ },
            ⋯⟩)
        e) =
    e