proposition: Lemma eq_inv_catl (u1 v1 : seq S) (u2 v2 : seq T) : eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> eq_inv u1 u2.
proof: Proof. move/eq_invP => []; rewrite !size_cat => Hsz Hinv Hszu. apply/eq_invP; split; first exact Hszu. move=> i j /andP[Hij Hj]. have /Hinv : i <= j < size u1 + size v1. by rewrite Hij /=; apply (leq_trans Hj); exact: leq_addr. by rewrite !nth_cat -Hszu Hj (leq_ltn_trans Hij Hj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp