proposition: Lemma filterCN (ltT : rel A) f t1 t2 : t1 \notin f -> {in f, forall z, ltT z t2 = (z == t1) || ltT z t1} -> filter (ltT^~ t2) f = filter (ltT^~ t1) f.
proof: Proof. move=>N C; apply: eq_in_filter=>x T; rewrite C ?inE ?orbT //. by case: eqP N T=>// -> /negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)