proposition: Lemma set_of_uniq (s : seq T) : uniq s -> perm_eq (set_of s) s.
proof: Proof. move => U. apply: uniq_perm (funiq _) U _ => x. exact: set_ofE. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)