As elementary as it is, let me ask the following question.
Given the theorem below, how does the proof function express the case the proposition p does not hold?
The implication, interpreted in its classical meaning, should still hold in this case.

variable {p : Prop}

theorem p_implies_p : p → p := (fun x => x)

I surely misunderstand the often mentioned proofs as programs correspondence, the idea of implications represented as functions in particular.

Thanks for any help.