Equality of decidable proofs? I want to know if the decidability of equality of two decidable proofs of the same proposition can be proved without any additional axioms in Calculus of Inductive Constructions.

Specifically, I want to know if this is true without any additional axioms in Coq.

$$\forall P: \texttt{Prop}, P \vee \neg P \Rightarrow
(\forall p_1 : P, \forall p_2: P, \{p_1 = p_2\} \vee \{p_1 \neq p_2\})
$$

Thanks!

Edited to correct the error:
Edit 2 to make Prop more explicit
As Neel points out if you work under the "propositions are types" then you can easily come up with a type whose equality cannot be shown decidable (but it is of course consistent to assume that all types have decidable equality), such as $\mathbb{N} \to \mathbb{N}$.

If we understand "proposition" as a more restricted kind of type, then the answer depends on what precisely we mean. If you are working in the calculus of constructions with a Prop kind then you still cannot show that decidable propositions have decidable equality. This is so because it is consistent in the calculus of constructions to equate Prop with a proof-relevant type universe, so for all you know Prop might contains something like $\mathbb{N} \to \mathbb{N}$. This also implies you cannot prove your theorem for Coq's notion of Prop.

But in any case, the best answer comes from homotopy type theory. There a proposition is a type $P$ which satisfies
$$\forall x, y : P \,.\, x = y.$$
That is, a proposition has at most one element (as it should if it is to be understood as a proof-irrelevant truth value). In this case the answer is of course positive because the definition of proposition immediately implies that its equality is decidable.

I am curious to know what you mean by "proposition".