proposition: Lemma subst_nmemSep (y:T) (A : {fset T}) (p : T -> bool): y \notin [ fset x in A | p x] -> y \notin A \/ ~~ p y.
proof: Proof. rewrite in_sep => P . apply: orP. by rewrite -negb_and. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)