diff --git a/theories/countable.v b/theories/countable.v
index 5f41b827d7b40e745117fe7c9f8f5bd86b74cc65..0d32ba0db9eb9fa8ff8c6b874257873d4a65a385 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -102,6 +102,11 @@ Section inj_countable'.
   Next Obligation. intros x. by f_equal/=. Qed.
 End inj_countable'.
 
+(** ** Empty *)
+Program Instance Empty_set_countable : Countable Empty_set :=
+  {| encode u := 1; decode p := None |}.
+Next Obligation. by intros []. Qed.
+
 (** ** Unit *)
 Program Instance unit_countable : Countable unit :=
   {| encode u := 1; decode p := Some () |}.
diff --git a/theories/decidable.v b/theories/decidable.v
index c5db311f9cb8567133e78c9d078b23c4be6adc65..2345ab9ff62c30c7d33fc542c09f438611f5d38c 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -184,6 +184,8 @@ Instance bool_eq_dec : EqDecision bool.
 Proof. solve_decision. Defined.
 Instance unit_eq_dec : EqDecision unit.
 Proof. solve_decision. Defined.
+Instance Empty_set_eq_dec : EqDecision Empty_set.
+Proof. solve_decision. Defined.
 Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
 Proof. solve_decision. Defined.
 Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
diff --git a/theories/finite.v b/theories/finite.v
index 4d8aba1fe051258a97560730152a0a299dc48025..154142362811dbc21560e738336f4f561c56b1a4 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -246,6 +246,12 @@ Qed.
 Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
 Proof. unfold card. simpl. by rewrite fmap_length. Qed.
 
+Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
+Next Obligation. by apply NoDup_nil. Qed.
+Next Obligation. intros []. Qed.
+Lemma Empty_set_card : card Empty_set = 0.
+Proof. done. Qed.
+
 Program Instance unit_finite : Finite () := {| enum := [tt] |}.
 Next Obligation. apply NoDup_singleton. Qed.
 Next Obligation. intros []. by apply elem_of_list_singleton. Qed.