proposition: Lemma subseq_uniqP s1 s2 : uniq s2 -> reflect (s1 = filter [in s1] s2) (subseq s1 s2).
proof: Proof. move=> uniq_s2; apply: (iffP idP) => [ss12 | ->]; last exact: filter_subseq. apply/eqP; rewrite -size_subseq_leqif ?subseq_filter ?(introT allP) //. apply/eqP/esym/perm_size. rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)