diff --git a/theories/base.v b/theories/base.v
index b046cf8e814a59f69444b04f98611140c266b996..370621e1054bd56d509a833e22f8de34345a81b3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
+Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+
 Class Top A := top : A.
 Notation "⊤" := top : C_scope.