proposition: Lemma eq_in_allpairs_dep f1 f2 s t : {in s, forall x, {in t x, f1 x =1 f2 x}} <-> [seq f1 x y : R | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].
proof: Proof. split=> [eq_f | eq_fst x s_x]. by congr flatten; apply/eq_in_map=> x s_x; apply/eq_in_map/eq_f. apply/eq_in_map; apply/eq_in_map: x s_x; apply/eq_from_flatten_shape => //. by rewrite /shape -!map_comp; apply/eq_map=> x /=; rewrite !size_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)