proposition: Lemma catCA_perm_ind P : (forall s1 s2 s3, P (s1 ++ s2 ++ s3) -> P (s2 ++ s1 ++ s3)) -> (forall s1 s2, perm_eq s1 s2 -> P s1 -> P s2).
proof: Proof. move=> PcatCA s1 s2 eq_s12; rewrite -[s1]cats0 -[s2]cats0. elim: s2 nil => [|x s2 IHs] s3 in s1 eq_s12 *. by case: s1 {eq_s12}(perm_size eq_s12). have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_mem eq_s12) mem_head. rewrite -(cat_take_drop i s1) -catA => /PcatCA. rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply. by rewrite -(perm_cons x) -def_s1 perm_rot. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)