From d167cced10a5db03b70318be4ffdf340e6bc52ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Sep 2017 21:55:34 +0200
Subject: [PATCH] Version of inj_countable with a total function.

---
 theories/countable.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/countable.v b/theories/countable.v
index 456ef2d4..4c2f6f03 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 () |}.
-- 
GitLab