proposition: Lemma eq_allpairsr (f : forall x, T x -> R) s t1 t2 : (forall x, t1 x = t2 x) -> [seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 x].
proof: Proof. by move=> eq_t; under eq_map do rewrite eq_t. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)