more instances for the empty type

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 () |}.

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).

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.