proposition: Lemma val_seq_sub_enum : uniq s -> map val seq_sub_enum = s.
proof: Proof. move=> Us; rewrite /seq_sub_enum undup_id ?pmap_sub_uniq //. rewrite (pmap_filter (insubK _)); apply/all_filterP. by apply/allP => x; rewrite isSome_insub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)