proposition: Lemma allrel_allpairsE xs ys : allrel xs ys = all id [seq r x y | x <- xs, y <- ys].
proof: Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)