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