proposition: Lemma perm_allpairs_dep f s1 t1 s2 t2 : perm_eq s1 s2 -> {in s1, forall x, perm_eq (t1 x) (t2 x)} -> perm_eq [seq f x y | x <- s1, y <- t1 x] [seq f x y | x <- s2, y <- t2 x].
proof: Proof. elim: s1 s2 t1 t2 => [s2 t1 t2 |a s1 IH s2 t1 t2 perm_s2 perm_t1]. by rewrite perm_sym => /perm_nilP->. have mem_a : a \in s2 by rewrite -(perm_mem perm_s2) inE eqxx. rewrite -[s2](cat_take_drop (index a s2)). rewrite allpairs_cat (drop_nth a) ?index_mem //= nth_index //=. rewrite perm_sym perm_catC -catA perm_cat //; last first. rewrite perm_catC -allpairs_cat. rewrite -remE perm_sym IH // => [|x xI]; last first. by apply: perm_t1; rewrite inE xI orbT. by rewrite -(perm_cons a) (perm_trans perm_s2 (perm_to_rem _)). have /perm_t1 : a \in a :: s1 by rewrite inE eqxx. rewrite perm_sym; elim: (t2 a) (t1 a) => /= [s4|b s3 IH1 s4 perm_s4]. by rewrite perm_sym => /perm_nilP->. have mem_b : b \in s4 by rewrite -(perm_mem perm_s4) inE eqxx. rewrite -[s4](cat_take_drop (index b s4)). rewrite map_cat /= (drop_nth b) ?index_mem //= nth_index //=. rewrite perm_sym perm_catC /= perm_cons // perm_catC -map_cat. rewrite -remE perm_sym IH1 // -(perm_cons b). by apply: perm_trans perm_s4 (perm_to_rem _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)