proposition: Lemma eq_allrel {T S : Type} (r r' : T -> S -> bool) : r =2 r' -> allrel r =2 allrel r'.
proof: Proof. by move=> rr' xs ys; apply/eq_in_allrel/all_predT/all_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)