proposition: Lemma perm_cons_cat_cons x s1 s2 s : perm (x :: s) (s1 ++ x :: s2) <-> perm s (s1 ++ s2).
proof: Proof. split=>[|H]; first by by move/(@perm_cat_consR [::] s s1 s2 x). by apply: (@perm_trans (x :: s1++s2))=>//; apply: permutation_skip eq_refl _. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)