proposition: Lemma eq_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) : {in P &, r =2 r'} -> forall xs, all P xs -> pairwise r xs = pairwise r' xs.
proof: Proof. move=> rr' xs Pxs. by apply/idP/idP; apply/sub_in_pairwise/Pxs => ? ? ? ?; rewrite rr'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)