proposition: Lemma catCA_perm_subst R F : (forall s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R) -> (forall s1 s2, perm_eq s1 s2 -> F s1 = F s2).
proof: Proof. move=> FcatCA s1 s2 /catCA_perm_ind => ind_s12. by apply: (ind_s12 (eq _ \o F)) => //= *; rewrite FcatCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)