proposition: Lemma eq_in_map (S : eqType) T (f g : S -> T) (s : seq S) : {in s, f =1 g} <-> map f s = map g s.
proof: Proof. by elim: s => //= x s IHs; rewrite forall_cons IHs; split => -[-> ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)