proposition: Lemma allrel_mapl {T T' S : Type} (f : T' -> T) (r : T -> S -> bool) xs ys : allrel r (map f xs) ys = allrel (fun x => r (f x)) xs ys.
proof: Proof. exact: all_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)