diff --git a/prelude/countable.v b/prelude/countable.v
index 6267748cf967cdf4b5a1d987cd0cfe718a50220e..a2aad6cc5181a3cab0679c9288d8e56d8a88cba4 100644
--- a/prelude/countable.v
+++ b/prelude/countable.v
@@ -78,6 +78,16 @@ Proof.
 Qed.
 
 (** * Instances *)
+(** ** Injection *)
+Section injective_countable.
+  Context `{Countable A, ∀ x y : B, Decision (x = y)}.
+  Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
+
+  Program Instance injective_countable : Countable B :=
+    {| encode y := encode (f y); decode p := x ← decode p; g x |}.
+  Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
+End injective_countable.
+
 (** ** Option *)
 Program Instance option_countable `{Countable A} : Countable (option A) := {|
   encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;