countable.v

Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound).
Proof.
  refine {| encode n := encode (to_N n);
            decode n := of_N =<< decode n; |}.
  intros [x lt].
  rewrite decode_encode.
  simpl.
  unfold of_N.
  destruct (BoundedN.N_lt_dec x bound).
  - assert (lt = l) by (apply UIP_dec; decide equality).
    congruence.
  - tauto.
Defined.