proposition: Lemma set_ofE x xs : (x \in set_of xs) = (x \in xs).
proof: Proof. rewrite -[x \in set_of xs]/(x \in fseq xs) -[x \in xs]mem_undup. symmetry. exact: (perm_mem (fseq_perm_eq _)). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)