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