proposition: Lemma allrel_relI {T S : Type} (r r' : T -> S -> bool) xs ys : allrel (fun x y => r x y && r' x y) xs ys = allrel r xs ys && allrel r' xs ys.
proof: Proof. by rewrite -all_predI; apply: eq_all => ?; rewrite /= -all_predI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)