proposition: Lemma eq_in_allpairs f1 f2 s t : {in s & t, f1 =2 f2} <-> [seq f1 x y : R | x <- s, y <- t] = [seq f2 x y | x <- s, y <- t].
proof: Proof. split=> [eq_f | /eq_in_allpairs_dep-eq_f x y /eq_f/(_ y)//]. by apply/eq_in_allpairs_dep=> x /eq_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)