proposition: Lemma satr_eqMem (a b : T) (A : {fset T}) : a == b -> b \in A -> a \in A.
proof: Proof. intros P Q. by rewrite -(eqP P) in Q. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)