Decidable

Let $P:A\to \mathrm{Prop}$ be a predicate.
We say that $P$ is decidable iff there is a procedure

$$f_P:(a:A)\to Pa\uplus \neg Pa$$

That produces a proof of $Pa$ or $\neg Pa$ for all $a$.