proposition: Lemma all_allpairsP (S : eqType) (T : S -> eqType) (R : Type) (p : pred R) (f : forall x : S, T x -> R) (s : seq S) (t : forall x : S, seq (T x)) : reflect (forall (x : S) (y : T x), x \in s -> y \in t x -> p (f x y)) (all p [seq f x y | x <- s, y <- t x]).
proof: Proof. elim: s => [|x s IHs]; first by constructor. rewrite /= all_cat all_map /preim. apply/(iffP andP)=> [[/allP /= ? ? x' y x'_in_xs]|p_xs_t]. by move: x'_in_xs y => /[1!inE] /predU1P [-> //|? ?]; exact: IHs. split; first by apply/allP => ?; exact/p_xs_t/mem_head. by apply/IHs => x' y x'_in_s; apply: p_xs_t; rewrite inE x'_in_s orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)