proposition: Lemma all_predC_sym xs ys : all [predC xs] ys = all [predC ys] xs.
proof: Proof. by rewrite all_predC has_sym -all_predC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)