proposition: Lemma eqEsub X Y : (X == Y) = (X `<=` Y) && (Y `<=` X).
proof: Proof. apply/eqP/andP => [-> //|[/subP H1 /subP H2]]. apply: fset_ext => x. apply/idP/idP; auto. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)