proposition: Lemma sep1 (a : T) (p : pred T) : [fset x in [fset a] | p x] = if p a then [fset a] else fset0.
proof: Proof. rewrite sepE fset1Es /= fun_if fset1E fset0E. by case: (p a). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)