proposition: Lemma sub_allrel {T S : Type} (r r' : T -> S -> bool) : (forall x y, r x y -> r' x y) -> forall xs ys, allrel r xs ys -> allrel r' xs ys.
proof: Proof. by move=> rr' xs ys; apply/sub_in_allrel/all_predT/all_predT; apply: in2W. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)