proposition: Lemma uniq_map_filter (T' T'' : eqType) (s : seq T') C (E : T' -> T'') : uniq [seq E i | i <- s] -> uniq [seq E i | i <- s & C i].
proof: Proof. elim s=> [//|h t IH] /= /andP [] Hh Ht. case (C h)=>/=; [|by apply IH]; apply/andP; split; [|by apply IH]. apply/negP=>H; move/negP in Hh; apply Hh; apply/mapP. move: H; move/mapP=> [] x Hx Hx'; exists x=>//; move: Hx. by rewrite mem_filter=>/andP []. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)