From mathcomp Require Import all_ssreflect finmap.

Section example.

Open Scope fset.

Variables (K : choiceType) (P : {fset K} -> Prop).

Lemma enum_fsetK (ks : {fset K}) :
  [fset k in enum_fset ks] = ks.
Proof.
  apply/fsetP => k; apply/imfsetP/idP => /=.
    by move=> [k' k'inks ->].
  by move=> kinks; exists k.
Qed.

Lemma fset_enum (ff : {fset K}) :
  P ff -> P [fset s in (enum_fset ff)].
Proof. by rewrite enum_fsetK. Qed.

(* So far so good. Now I want to use fset_enum in the wild... *)
Lemma Ps_seq (ff : {fset K}) :
  P ff -> exists (ss : seq K), P [fset s in ss].
Proof.
  move=> /fset_enum Pff.
  exists (enum_fset ff).
  Fail exact: Pff. (* ... but alas, this doesn't work *)
  set X := [fset _ in _] in Pff. (* X := [fset H in fset_finpred ff] : {fset K} *)
  set Y := [fset _ in _]. (* Y := [fset H in fin_finpred (pT:=seq_finpredType K) ff] : {fset K} *)
(* so indeed X and Y are different, although we can easily prove they are the same: *)
  suff <- : X = Y by [].
  by apply/fsetP => x; apply/imfsetP/imfsetP.
Qed.

End example.

Lemma fin_fset_finpred (ff : {fset K}) :
  [fset f in fin_finpred (pT:=seq_finpredType K) ff]
    = [fset f in fset_finpred ff].
Proof. by apply/fsetP => f; apply/imfsetP/imfsetP. Qed.