diff --git a/theories/countable.v b/theories/countable.v
new file mode 100644
index 0000000000000000000000000000000000000000..1ea69bda5b6d5f946c46ab79c03390207a6d68cf
--- /dev/null
+++ b/theories/countable.v
@@ -0,0 +1,229 @@
+Require Export list.
+Local Obligation Tactic := idtac.
+Local Open Scope positive.
+
+Class Countable A `{∀ x y : A, Decision (x = y)} := {
+  encode : A → positive;
+  decode : positive → option A;
+  decode_encode x : decode (encode x) = Some x
+}.
+
+Definition encode_nat `{Countable A} (x : A) : nat :=
+  pred (Pos.to_nat (encode x)).
+Definition decode_nat `{Countable A} (i : nat) : option A :=
+  decode (Pos.of_nat (S i)).
+Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
+Proof.
+  pose proof (Pos2Nat.is_pos (encode x)).
+  unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
+  by rewrite Pos2Nat.id, decode_encode.
+Qed.
+
+Section choice.
+  Context `{Countable A} (P : A → Prop) `{∀ x, Decision (P x)}.
+
+  Inductive choose_step: relation positive :=
+    | choose_step_None {p} : decode p = None → choose_step (Psucc p) p
+    | choose_step_Some {p x} :
+       decode p = Some x → ¬P x → choose_step (Psucc p) p.
+
+  Lemma choose_step_acc : (∃ x, P x) → Acc choose_step 1%positive.
+  Proof.
+    intros [x Hx]. cut (∀ i p,
+      i ≤ encode x → 1 + encode x = p + i → Acc choose_step p).
+    { intros help. by apply (help (encode x)). }
+    induction i as [|i IH] using Pos.peano_ind; intros p ??.
+    { constructor. intros j. assert (p = encode x) by lia; subst.
+      inversion 1 as [? Hd|?? Hd]; subst;
+        rewrite decode_encode in Hd; congruence. }
+    constructor. intros j.
+    inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
+  Qed.
+
+  Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
+    match Some_dec (decode i) with
+    | inleft (x↾Hx) =>
+      match decide (P x) with
+      | left _ => x
+      | right H => choose_go (Acc_inv acc (choose_step_Some Hx H))
+      end
+    | inright H => choose_go (Acc_inv acc (choose_step_None H))
+    end.
+  Fixpoint choose_go_correct {i} (acc : Acc choose_step i) : P (choose_go acc).
+  Proof. destruct acc; simpl. repeat case_match; auto. Qed.
+  Fixpoint choose_go_pi {i} (acc1 acc2 : Acc choose_step i) :
+    choose_go acc1 = choose_go acc2.
+  Proof. destruct acc1, acc2; simpl; repeat case_match; auto. Qed.
+
+  Definition choose (H: ∃ x, P x) : A := choose_go (choose_step_acc H).
+  Definition choose_correct (H: ∃ x, P x) : P (choose H) := choose_go_correct _.
+  Definition choose_pi (H1 H2 : ∃ x, P x) :
+    choose H1 = choose H2 := choose_go_pi _ _.
+  Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
+End choice.
+
+Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
+  (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
+Proof.
+  exists (λ y, choose (λ x, f x = y) (surjective f y)).
+  intros y. by rewrite (choose_correct _ (surjective f y)).
+Qed.
+
+(** ** Instances *)
+Program Instance option_countable `{Countable A} : Countable (option A) := {|
+  encode o :=
+    match o with None => 1 | Some x => Pos.succ (encode x) end;
+  decode p :=
+    if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
+|}.
+Next Obligation.
+  intros ??? [x|]; simpl; repeat case_decide; auto with lia.
+  by rewrite Pos.pred_succ, decode_encode.
+Qed.
+
+Program Instance sum_countable `{Countable A} `{Countable B} :
+  Countable (A + B)%type := {|
+    encode xy :=
+      match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
+    decode p :=
+      match p with
+      | 1 => None | p~0 => inl <$> decode p | p~1 => inr <$> decode p
+      end
+  |}.
+Next Obligation. by intros ?????? [x|y]; simpl; rewrite decode_encode. Qed.
+
+Fixpoint prod_encode_fst (p : positive) : positive :=
+  match p with
+  | 1 => 1
+  | p~0 => (prod_encode_fst p)~0~0
+  | p~1 => (prod_encode_fst p)~0~1
+  end.
+Fixpoint prod_encode_snd (p : positive) : positive :=
+  match p with
+  | 1 => 1~0
+  | p~0 => (prod_encode_snd p)~0~0
+  | p~1 => (prod_encode_snd p)~1~0
+  end.
+Fixpoint prod_encode (p q : positive) : positive :=
+  match p, q with
+  | 1, 1 => 1~1
+  | p~0, 1 => (prod_encode_fst p)~1~0
+  | p~1, 1 => (prod_encode_fst p)~1~1
+  | 1, q~0 => (prod_encode_snd q)~0~1
+  | 1, q~1 => (prod_encode_snd q)~1~1
+  | p~0, q~0 => (prod_encode p q)~0~0
+  | p~0, q~1 => (prod_encode p q)~1~0
+  | p~1, q~0 => (prod_encode p q)~0~1
+  | p~1, q~1 => (prod_encode p q)~1~1
+  end.
+Fixpoint prod_decode_fst (p : positive) : option positive :=
+  match p with
+  | p~0~0 => (~0) <$> prod_decode_fst p
+  | p~0~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
+  | p~1~0 => (~0) <$> prod_decode_fst p
+  | p~1~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
+  | 1~0 => None
+  | 1~1 => Some 1
+  | 1 => Some 1
+  end.
+Fixpoint prod_decode_snd (p : positive) : option positive :=
+  match p with
+  | p~0~0 => (~0) <$> prod_decode_snd p
+  | p~0~1 => (~0) <$> prod_decode_snd p
+  | p~1~0 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
+  | p~1~1 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
+  | 1~0 => Some 1
+  | 1~1 => Some 1
+  | 1 => None
+  end.
+
+Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
+Proof.
+  assert (∀ p, prod_decode_fst (prod_encode_fst p) = Some p).
+  { intros p'. by induction p'; simplify_option_equality. }
+  assert (∀ p, prod_decode_fst (prod_encode_snd p) = None).
+  { intros p'. by induction p'; simplify_option_equality. }
+  revert q. by induction p; intros [?|?|]; simplify_option_equality.
+Qed.
+Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
+Proof.
+  assert (∀ p, prod_decode_snd (prod_encode_snd p) = Some p).
+  { intros p'. by induction p'; simplify_option_equality. }
+  assert (∀ p, prod_decode_snd (prod_encode_fst p) = None).
+  { intros p'. by induction p'; simplify_option_equality. }
+  revert q. by induction p; intros [?|?|]; simplify_option_equality.
+Qed.
+Program Instance prod_countable `{Countable A} `{Countable B} :
+  Countable (A * B)%type := {|
+    encode xy := let (x,y) := xy in prod_encode (encode x) (encode y);
+    decode p :=
+     x ← prod_decode_fst p ≫= decode;
+     y ← prod_decode_snd p ≫= decode; Some (x, y)
+  |}.
+Next Obligation.
+  intros ?????? [x y]; simpl.
+  rewrite prod_decode_encode_fst, prod_decode_encode_snd.
+  simpl. by rewrite !decode_encode.
+Qed.
+
+Fixpoint list_encode_ (l : list positive) : positive :=
+  match l with [] => 1 | x :: l => prod_encode x (list_encode_ l) end.
+Definition list_encode (l : list positive) : positive :=
+  prod_encode (Pos.of_nat (S (length l))) (list_encode_ l).
+
+Fixpoint list_decode_ (n : nat) (p : positive) : option (list positive) :=
+  match n with
+  | O => guard (p = 1); Some []
+  | S n =>
+     x ← prod_decode_fst p; pl ← prod_decode_snd p;
+     l ← list_decode_ n pl; Some (x :: l)
+  end.
+Definition list_decode (p : positive) : option (list positive) :=
+  pn ← prod_decode_fst p; pl ← prod_decode_snd p;
+  list_decode_ (pred (Pos.to_nat pn)) pl.
+
+Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
+Proof.
+  cut (list_decode_ (length l) (list_encode_ l) = Some l).
+  { intros help. unfold list_decode, list_encode.
+    rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
+    by rewrite Nat2Pos.id by done; simpl. }
+  induction l; simpl; auto.
+  by rewrite prod_decode_encode_fst, prod_decode_encode_snd;
+    simplify_option_equality.
+Qed.
+
+Program Instance list_countable `{Countable A} : Countable (list A) :=  {|
+  encode l := list_encode (encode <$> l);
+  decode p := list_decode p ≫= mapM decode
+|}.
+Next Obligation.
+  intros ??? l. rewrite list_decode_encode. simpl.
+  apply mapM_fmap_Some; auto using decode_encode.
+Qed.
+
+Program Instance pos_countable : Countable positive := {|
+  encode := id; decode := Some; decode_encode x := eq_refl
+|}.
+Program Instance N_countable : Countable N := {|
+  encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
+  decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
+|}.
+Next Obligation.
+  intros [|p]; simpl; repeat case_decide; auto with lia.
+  by rewrite Pos.pred_succ.
+Qed.
+Program Instance Z_countable : Countable Z := {|
+  encode x :=
+    match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
+  decode p := Some
+    match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
+|}.
+Next Obligation. by intros [|p|p]. Qed.
+Program Instance nat_countable : Countable nat := {|
+  encode x := encode (N.of_nat x);
+  decode p := N.to_nat <$> decode p
+|}.
+Next Obligation.
+  intros x. rewrite decode_encode; simpl. by rewrite Nat2N.id.
+Qed.
diff --git a/theories/finite.v b/theories/finite.v
new file mode 100644
index 0000000000000000000000000000000000000000..6c3a5f55b5fddb25cb56072c8cfab2e0c6b03cf2
--- /dev/null
+++ b/theories/finite.v
@@ -0,0 +1,274 @@
+Require Export countable list.
+Obligation Tactic := idtac.
+
+Class Finite A `{∀ x y : A, Decision (x = y)} := {
+  enum : list A;
+  enum_nodup : NoDup enum;
+  elem_of_enum x : x ∈ enum
+}.
+Arguments enum _ {_ _} : clear implicits.
+Arguments enum_nodup _ {_ _} : clear implicits.
+Definition card A `{Finite A} := length (enum A).
+Program Instance finite_countable `{Finite A} : Countable A := {|
+  encode := λ x, Pos.of_nat $ S $ from_option 0 $ list_find (x =) (enum A);
+  decode := λ p, enum A !! pred (Pos.to_nat p)
+|}.
+Arguments Pos.of_nat _ : simpl never.
+Next Obligation.
+  intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
+  destruct (list_find_eq_elem_of xs x) as [i Hi]; auto.
+  rewrite Nat2Pos.id by done; simpl.
+  rewrite Hi; eauto using list_find_eq_Some.
+Qed.
+Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A :=
+  list_find P (enum A) ≫= decode_nat.
+
+Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A.
+Proof.
+  destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
+  rewrite Nat2Pos.id by done; simpl. destruct (list_find _ xs) eqn:?; simpl.
+  * eapply lookup_lt_Some, list_find_eq_Some; eauto.
+  * destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
+Qed.
+Lemma encode_decode A `{finA: Finite A} i :
+  i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i.
+Proof.
+  destruct finA as [xs Hxs HA].
+  unfold encode_nat, decode_nat, encode, decode, card; simpl.
+  intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
+  exists x. rewrite !Nat2Pos.id by done; simpl.
+  destruct (list_find_eq_elem_of xs x) as [j Hj]; auto.
+  rewrite Hj. eauto using list_find_eq_Some, NoDup_lookup.
+Qed.
+Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
+  find P = Some x → P x.
+Proof.
+  destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
+  intros Hx. destruct (list_find _ _) as [i|] eqn:Hi; simplify_option_equality.
+  rewrite !Nat2Pos.id in Hx by done.
+  destruct (list_find_Some P xs i) as (?&?&?); simplify_option_equality; eauto.
+Qed.
+Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
+  P x → ∃ y, find P = Some y ∧ P y.
+Proof.
+  destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
+  intros Hx. destruct (list_find_elem_of P xs x) as [i Hi]; auto.
+  rewrite Hi. destruct (list_find_Some P xs i) as (y&?&?); subst; auto.
+  exists y. simpl. by rewrite !Nat2Pos.id by done.
+Qed.
+
+Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P.
+Proof.
+  intros ? x. destruct finA as [[|??] ??]; simplify_equality.
+  by destruct (not_elem_of_nil x).
+Qed.
+Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A.
+Proof.
+  unfold card. destruct finA as [[|x ?] ??]; simpl; auto with lia.
+  constructor; exact x.
+Qed.
+Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)
+  `{!Injective (=) (=) f} : f <$> enum A `contains` enum B.
+Proof.
+  intros. destruct finA, finB. apply NoDup_contains; auto using fmap_nodup_2.
+Qed.
+Lemma finite_injective_Permutation `{Finite A} `{Finite B} (f : A → B)
+  `{!Injective (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
+Proof.
+  intros. apply contains_Permutation.
+  * by rewrite fmap_length.
+  * by apply finite_injective_contains.
+Qed.
+Lemma finite_injective_surjective `{Finite A} `{Finite B} (f : A → B)
+  `{!Injective (=) (=) f} : card A = card B → Surjective (=) f.
+Proof.
+  intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
+  rewrite finite_injective_Permutation; auto using elem_of_enum.
+Qed.
+
+Lemma finite_surjective A `{Finite A} B `{Finite B} :
+  0 < card A ≤ card B → ∃ g : B → A, Surjective (=) g.
+Proof.
+  intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
+  exists (λ y : B, from_option x' (decode_nat (encode_nat y))).
+  intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2).
+  { pose proof (encode_lt_card x); lia. }
+  exists y. by rewrite Hy2, decode_encode_nat.
+Qed.
+Lemma finite_injective A `{Finite A} B `{Finite B} :
+  card A ≤ card B ↔ ∃ f : A → B, Injective (=) (=) f.
+Proof.
+  split.
+  * intros. destruct (decide (card A = 0)) as [HA|?].
+    { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
+    destruct (finite_surjective A B) as (g&?); auto with lia.
+    destruct (surjective_cancel g) as (f&?). exists f. apply cancel_injective.
+  * intros [f ?]. unfold card. rewrite <-(fmap_length f).
+    by apply contains_length, (finite_injective_contains f).
+Qed.
+Lemma finite_bijective A `{Finite A} B `{Finite B} :
+  card A = card B ↔ ∃ f : A → B, Injective (=) (=) f ∧ Surjective (=) f.
+Proof.
+  split.
+  * intros; destruct (proj1 (finite_injective A B)) as [f ?]; auto with lia.
+    exists f; auto using (finite_injective_surjective f).
+  * intros (f&?&?). apply (anti_symmetric (≤)); apply finite_injective.
+    + by exists f.
+    + destruct (surjective_cancel f) as (g&?); eauto using cancel_injective.
+Qed.
+Lemma injective_card `{Finite A} `{Finite B} (f : A → B)
+  `{!Injective (=) (=) f} : card A ≤ card B.
+Proof. apply finite_injective. eauto. Qed.
+Lemma surjective_card `{Finite A} `{Finite B} (f : A → B)
+  `{!Surjective (=) f} : card B ≤ card A.
+Proof.
+  destruct (surjective_cancel f) as (g&?).
+  apply injective_card with g, cancel_injective.
+Qed.
+Lemma bijective_card `{Finite A} `{Finite B} (f : A → B)
+  `{!Injective (=) (=) f} `{!Surjective (=) f} : card A = card B.
+Proof. apply finite_bijective. eauto. Qed.
+
+(** Instances *)
+Section enc_finite.
+  Context `{∀ x y : A, Decision (x = y)}.
+  Context (to_nat : A → nat) (of_nat : nat → A) (c : nat).
+  Context (of_to_nat : ∀ x, of_nat (to_nat x) = x).
+  Context (to_nat_c : ∀ x, to_nat x < c).
+  Context (to_of_nat : ∀ i, i < c → to_nat (of_nat i) = i).
+
+  Program Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
+  Next Obligation.
+    apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
+    destruct (seq _ _ !! i) as [i'|] eqn:Hi',
+      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality.
+    destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
+    rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
+  Qed.
+  Next Obligation.
+    intros x. rewrite elem_of_list_fmap. exists (to_nat x).
+    split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
+  Qed.
+  Lemma enc_finite_card : card A = c.
+  Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
+End enc_finite.
+
+Section bijective_finite.
+  Context `{Finite A} `{∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A).
+  Context `{!Injective (=) (=) f} `{!Cancel (=) f g}.
+
+  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
+  Next Obligation. apply (fmap_nodup _), enum_nodup. Qed.
+  Next Obligation.
+    intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum.
+  Qed.
+End bijective_finite.
+
+Program Instance option_finite `{Finite A} : Finite (option A) :=
+  {| enum := None :: Some <$> enum A |}.
+Next Obligation.
+  constructor.
+  * rewrite elem_of_list_fmap. by intros (?&?&?).
+  * apply (fmap_nodup _); auto using enum_nodup.
+Qed.
+Next Obligation.
+  intros ??? [x|]; [right|left]; auto.
+  apply elem_of_list_fmap. eauto using elem_of_enum.
+Qed.
+Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
+Proof. unfold card. simpl. by rewrite fmap_length. Qed.
+
+Program Instance unit_finite : Finite () := {| enum := [tt] |}.
+Next Obligation. apply NoDup_singleton. Qed.
+Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
+Lemma unit_card : card unit = 1.
+Proof. done. Qed.
+
+Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
+Next Obligation.
+  constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton.
+Qed.
+Next Obligation. intros [|]. left. right; left. Qed.
+Lemma bool_card : card bool = 2.
+Proof. done. Qed.
+
+Program Instance sum_finite `{Finite A} `{Finite B} : Finite (A + B)%type :=
+  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
+Next Obligation.
+  intros. apply NoDup_app; split_ands.
+  * apply (fmap_nodup _). by apply enum_nodup.
+  * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
+  * apply (fmap_nodup _). by apply enum_nodup.
+Qed.
+Next Obligation.
+  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
+    eauto using @elem_of_enum.
+Qed.
+Lemma sum_card `{Finite A} `{Finite B} : card (A + B) = card A + card B.
+Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
+
+Program Instance prod_finite `{Finite A} `{Finite B} : Finite (A * B)%type :=
+  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
+Next Obligation.
+  intros ??????. induction (enum_nodup A) as [|x xs Hx Hxs IH]; simpl.
+  { constructor. }
+  apply NoDup_app; split_ands.
+  * apply (fmap_nodup _). by apply enum_nodup.
+  * intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
+    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
+    { rewrite elem_of_nil. tauto. }
+    rewrite elem_of_app, elem_of_list_fmap.
+    intros [(?&?&?)|?]; simplify_equality.
+    + destruct Hx. by left.
+    + destruct IH. by intro; destruct Hx; right. auto.
+  * done.
+Qed.
+Next Obligation.
+  intros ?????? [x y]. induction (elem_of_enum x); simpl.
+  * rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
+  * rewrite elem_of_app; eauto.
+Qed.
+Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
+Proof.
+  unfold card; simpl. induction (enum A); simpl; auto.
+  rewrite app_length, fmap_length. auto.
+Qed.
+
+Let list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } :=
+  fix go n :=
+  match n with
+  | 0 => [[]↾eq_refl]
+  | S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
+  end.
+Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
+  {| enum := list_enum (enum A) n |}.
+Next Obligation.
+  intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
+  revert IH. generalize (list_enum (enum A) n). intros l Hl.
+  induction (enum_nodup A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
+  apply NoDup_app; split_ands.
+  * by apply (fmap_nodup _).
+  * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
+    intros ([k2 Hk2]&?&?) Hxk2; simplify_equality. destruct Hx. revert Hxk2.
+    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
+    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
+    intros [([??]&?&?)|?]; simplify_equality; auto.
+  * apply IH.
+Qed.
+Next Obligation.
+  intros ???? [l Hl]. revert l Hl.
+  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_equality.
+  { apply elem_of_list_singleton. by apply (sig_eq_pi _). }
+  revert IH. generalize (list_enum (enum A) n). intros k Hk.
+  induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
+  * rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
+    eexists (l↾Hl'). split. by apply (sig_eq_pi _). done.
+  * rewrite elem_of_app. eauto.
+Qed.
+Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
+Proof.
+  unfold card; simpl. induction n as [|n IH]; simpl; auto.
+  rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
+  induction (enum A) as [|x xs IH]; intros l; simpl; auto.
+  by rewrite app_length, fmap_length, IH.
+Qed.