proposition: Lemma perm_cons_catCA s1 s2 x : perm (x :: s1 ++ s2) (s1 ++ x :: s2).
proof: Proof. rewrite -cat_rcons -cats1 -cat_cons -cat1s. by apply: perm_cat2rL; apply: perm_catC. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)