proposition: Lemma perm_pmap s t : perm_eq s t -> perm_eq (pmap f s) (pmap f t).
proof: Proof. move=> eq_st; apply/(perm_map_inj Some_inj); rewrite !pmapS_filter. exact/perm_map/perm_filter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)