proposition: Lemma get_filterf f P k (kff : k \in filterf f P) (kf : k \in f) : (filterf f P).[kff] = f.[kf].
proof: Proof. apply: Some_inj; rewrite !Some_fnd /= fnd_filterf. by move: kff; rewrite !(in_fset, inE) => /andP [? ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)