diff --git a/theories/base.v b/theories/base.v
index a94511d4ee56c63cb11a0a57bacb8eaa5c7b8523..36af265f23b0aa8104346cc983c5faa727619ec8 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -129,7 +129,7 @@ Arguments decide _ {_}.
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
-Class Inhabited (A : Type) : Prop := populate { _ : A }.
+Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Arguments populate {_} _.
Instance unit_inhabited: Inhabited unit := populate ().
diff --git a/theories/finite.v b/theories/finite.v
index 7824001163d1cb787b7641ee2cf5dcb50ebd298b..fed9dd3f795fd9e68de56e561956edf16c007731 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -69,7 +69,7 @@ Proof.
Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A.
Proof.
- unfold card. destruct finA as [[|x ?] ??]; simpl; auto with lia.
+ unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
constructor; exact x.
Qed.
Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)