proposition: Lemma eq_In_filter (T : Type) a1 a2 (s : seq T) : (forall x, x \In s -> a1 x = a2 x) -> filter a1 s = filter a2 s.
proof: Proof. elim: s => //= x s IHs eq_a. rewrite eq_a; last by rewrite InE; left. rewrite IHs // => y s_y; apply: eq_a. by rewrite InE; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)