proposition: Lemma sizes_eq0 X : (size X == 0) = (X == fset0).
proof: Proof. apply/idP/eqP => [|->]; last by rewrite sizes0. rewrite -leqn0 -sizes0 => H. symmetry. exact: subsize_eq. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)