Library discprob.basic.classic_proof_irrel

Require Import ClassicalFacts Classical_Prop ProofIrrelevanceFacts.

Lemma classical_proof_irrelevance : ∀ (P : Prop) (p1 p2 : P), p1 = p2.

Module PI. Definition proof_irrelevance := classical_proof_irrelevance. End PI.

Module PIT := ProofIrrelevanceTheory(PI).
Export PIT.