proposition: Lemma subst_memSep (y:T) (A : {fset T}) (p : T -> bool) : y \in sep A p -> (y \in A) /\ (p y).
proof: Proof. rewrite in_sep. apply: andP. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)