diff --git a/theories/base.v b/theories/base.v
index dfedf6f0d22aa3cafa31cc1dcf6e4046d2e0b735..30feccb2b6759ea57976109a1017f33b460b4069 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -413,6 +413,8 @@ Class TotalOrder {A} (R : relation A) : Prop := {
 }.
 
 (** * Logic *)
+Instance prop_inhabited : Inhabited Prop := populate True.
+
 Notation "(∧)" := and (only parsing) : stdpp_scope.
 Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
 Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope.