proposition: Lemma allrelP {T S : eqType} {r : T -> S -> bool} {xs ys} : reflect {in xs & ys, forall x y, r x y} (allrel r xs ys).
proof: Proof. by rewrite allrel_allpairsE; exact: all_allpairsP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)