proposition: Lemma fset_eq X Y : X =i Y -> X == Y :> {fset T}.
proof: Proof. move: X Y => [xs ax_xs] [ys ax_ys] /= H. change (xs == ys). change (xs =i ys) in H. case/andP : ax_xs ax_ys => xs1 /eqP -> /andP [ys1 /eqP ->]. have ext : perm_eql xs ys by apply/permPl/uniq_perm. rewrite -(eq_choose ext). apply/eqP/choose_id => //. exact/permPl. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)