proposition: Lemma filter_predIC {A} (s : seq A) p1 p2 : filter (predI p1 p2) s = filter (predI p2 p1) s.
proof: Proof. by apply: eq_filter => z /=; rewrite andbC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)