> With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.

Here's another way to explain this:

As you state, Prop has to do with proof-irrelevance. When doing constructive mathematics, proofs are programs (meaning they carry computational content), but sometimes it's useful to treat any two proofs of the same proposition as equal. As a consequence, proofs cannot be inspected or run as programs, and you get back the Law of Excluded Middle from classical mathematics.

Decidable has to do with decidability. This means that given some proposition P, there is an algorithm that can either produce a proof of P, or a proof of ~P. This is usually useful when P is a predicate, so that at each x, P(x) either has a proof or a disproof.

In classical mathematics, the Law of Excluded Middle holds for all propositions. In constructive mathematics, the Law of Excluded Middle only holds for decidable propositions. If P is decidable, it is safe to constructively assume P or ~P because an algorithm can produce the answer.