proposition: Lemma eq (s s' : seq K) : s =i s' <-> f s = f s'.
proof: Proof. split=> [eq_ss'|eq_ss' k]; last by rewrite -E eq_ss' E. rewrite /f; have peq_ss' : perm_eq (undup s) (undup s'). by apply: uniq_perm; rewrite ?undup_uniq // => x; rewrite !mem_undup. rewrite (@choose_id _ _ _ (undup s')) //=; apply: eq_choose => x /=. by apply: sym_left_transitive; [exact: perm_sym | exact: (@perm_trans)|]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)