proposition: Lemma fseq_axiom (xs : seq T) : fset_axiom (fseq xs).
proof: Proof. rewrite /fset_axiom /= fseq_uniq /= {1}/fseq /=. apply/eqP. have P := permPl (fseq_perm_eq xs). rewrite -(eq_choose P). apply: choose_id => //. exact: fseq_perm_eq. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)