proposition: Lemma inj_in_map (A : {pred T1}) : {in A &, injective f} -> {in [pred s | all [in A] s] &, injective map}.
proof: Proof. move=> injf; elim=> [|x s IHs] [|y t] //= /andP[Ax As] /andP[Ay At]. by case=> /injf-> // /IHs->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)