Provably finite sets in constructivist logic

Question

I was reading about Diaconescu's theorem and began with the following statement: If for a given proposition $P$ we let $U=\lbrace x \in \lbrace 0,1 \rbrace : (x=0) \lor P \rbrace$, then $U$ is not provably finite (using constructivist logic). Why is this?

Answer 1

If $P$ holds, then $U=\{0,1\}$, otherwise $U=\{0\}$. Your task is to exhibit a bijection with a finite ordinal. If $P$ is such that you don't know if $P$ is true or not, you cannot exhibit a bijection $1\to U$ nor a bijection $2\to U$. In fact any such (provable) bijection would give us a proof of $P$ or $\neg P$, respectively.