proposition: Lemma fsizeU1 (T : choiceType) x (X : {fset T}) : size (x |` X) <= (size X).+1.
proof: Proof. rewrite -addn1 addnC. apply: leq_trans (fsizeU _ _) _. by rewrite fset1Es. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)