diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index af527c74412ecdb4cc1c84f6bcab21f9e191468b..9b2bbc38984c01704d992bde7cc3abfa5a4ae387 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -8,6 +8,8 @@ Instance True_pi: ProofIrrel True.
 Proof. intros [] []; reflexivity. Qed.
 Instance False_pi: ProofIrrel False.
 Proof. intros []. Qed.
+Instance unit_pi: ProofIrrel ().
+Proof. intros [] []; reflexivity. Qed.
 Instance and_pi (A B : Prop) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
 Proof. intros ?? [??] [??]. f_equal; trivial. Qed.