proposition: Lemma subsize_eq X Y : X `<=` Y -> size Y <= size X -> X = Y.
proof: Proof. move => /subP S H. apply: fset_ext. apply uniq_min_size => //. exact: funiq. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)