proposition: Lemma satr_memSub (a:T) (A B : {fset T}) : a \in A -> A `<=` B -> a \in B.
proof: Proof. move => P Q. apply: (@subP T A) => //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)