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