proposition: Lemma perm_cons x s1 s2 : perm (x :: s1) (x :: s2) <-> perm s1 s2.
proof: Proof. split; last by apply: permutation_skip. by move/(@perm_cat_consR [::] s1 [::] s2 x). Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)