proposition: Lemma sub_pairwise {T : Type} (r r' : rel T) xs : subrel r r' -> pairwise r xs -> pairwise r' xs.
proof: Proof. by move=> rr'; apply/sub_in_pairwise/all_predT; apply: in2W. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)