proposition: Lemma imfset_rec (T : choiceType) (f : T -> K) (p : finmempred T) (P : imfset key f p -> Prop) : (forall (x : T) (px : in_mem x p), P [` in_imfset f px ]) -> forall k, P k.
proof: Proof. move=> PP v; have /imfsetP [k pk vv_eq] := valP v. pose vP := in_imfset f pk; suff -> : P v = P [` vP] by apply: PP. by congr P; apply/val_inj => /=; rewrite -vv_eq . Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)