What types are propositions?
The original conception of propositions-as-types did not distinguish propositions and types at all: all types are propositions. Under this view, we may indeed speak of different proofs of a proposition.

One way to understand the differences between different conceptions of propositions-as-types is to view them as capturing different notions of provability and truth:


If we say that Prop = Type then the elements of a proposition are the proofs, so we are capturing proof constructions. We may analyze proofs, and for instance distinguish them according to their size, the assumptions they use, etc.
If we say that Prop = HProp then the elements of a proposition witness existence of proofs (but are not specific proofs), so we are capturing provabillity. We can still discern the reason for a proposition being true, because we can analyze the proof as lons as further constructions do not depend on the choice of proof.
If we use the strict SProp which makes all proofs judgmentally equal (or simply erases proof altogether), then inside type theory we can never "discern" the reasons for a proposition being true, so this is more like truth, i.e., an external reason for something being the case. We do have soundness in the sense that type theory can express semantic entailment, e.g., if $p$ and $q$ are true then so is $p \land q$.


Coqs Prop is conservative in the sense that it makes no commitment as to what Prop is supposed to be. Coq is compatible with the view that Prop is an (impredicative) Type, as well as that it is something like HProp, or even just bool. This is a design decision.