proposition: Lemma perm_cat_consL s1 t1 s2 t2 x : perm s1 s2 -> perm t1 t2 -> perm (s1 ++ x :: t1) (s2 ++ x :: t2).
proof: Proof. by move=>H1 H2; apply: perm_catL H1 _; apply: permutation_skip H2. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)