diff --git a/theories/base.v b/theories/base.v
index 72d51f9be294ab9b8918463d178a220e2b98b648..ff635a1a3cf0bc5b84a3fc2ba9aff9572e0f34cd 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -306,6 +306,9 @@ Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
 Notation "(∘ f )" := (λ g, compose g f) (only parsing) : C_scope.
 
+Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
+  populate (λ _, inhabitant).
+
 (** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
 applied. *)
 Arguments id _ _ /.