proposition: Lemma uniq_predom_reduce s : uniq (predom (reduce s)).
proof: Proof. rewrite /reduce; set s' := (foldr _ _ _). apply: (subseq_uniq (s2 := predom s')). exact/map_subseq/filter_subseq. by rewrite {}/s'; elim: s=> [|[z x] s IHs] //=; exact: uniq_predom_augment. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)