proposition: Lemma filter2CN (ltT : rel A) p f t1 t2 : t1 \notin p -> {in p, forall z, ltT z t2 = (z == t1) || ltT z t1} -> filter (ltT^~ t2) (filter p f) = filter (ltT^~ t1) (filter p f).
proof: Proof. move=>N C; apply: filterCN; first by rewrite mem_filter negb_and N. by move=>z; rewrite mem_filter=>/andP [D _]; apply: C. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)