∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : Finite ↑{x | p x}]
  (e : { x // p x } ≃ { x // q x }) (x : α) (hx : ¬p x), e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)