proposition: Lemma fset1U x : x \in X -> X = x |` X.
proof: Proof. move => inX. apply/fset_ext => y. rewrite !inE. by case (boolP (y == x)) => //= /eqP ->. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)