proposition: Lemma filter_mem_sym (s1 s2 : seq A) : filter (mem s1) s2 =i filter (mem s2) s1.
proof: Proof. by move=>x; rewrite !mem_filter andbC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)