proposition: Lemma satr_nmemU (a:T) (A B : {fset T}) : a \notin A `|` B -> a \notin A /\ a \notin B.
proof: Proof. rewrite in_fsetU negb_or. apply: andP. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)