proposition: Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) : {f | uniq s -> size fs = size s -> map f s = fs}.
proof: Proof. exists (fun x => nth y0 fs (index x s)) => uAs eq_sz. apply/esym/(@eq_from_nth _ y0); rewrite ?size_map eq_sz // => i ltis. by have x0 : T1 by [case: (s) ltis]; rewrite (nth_map x0) // index_uniq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)