diff --git a/theories/countable.v b/theories/countable.v
index 456ef2d48c5f4e9169144eb09dded35ee0c7c132..4c2f6f03bd900780900c55b91efeaf2700b69c20 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -93,6 +93,14 @@ Section inj_countable.
   Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
 End inj_countable.
 
+Section inj_countable'.
+  Context `{Countable A, EqDecision B}.
+  Context (f : B → A) (g : A → B) (fg : ∀ x, g (f x) = x).
+
+  Program Instance inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
+  Next Obligation. intros x. by f_equal/=. Qed.
+End inj_countable'.
+
 (** ** Unit *)
 Program Instance unit_countable : Countable unit :=
   {| encode u := 1; decode p := Some () |}.