proposition: Lemma pperm_cat_consL s1 t1 s2 t2 x : perm s1 s2 -> perm t1 t2 -> perm (s1 ++ x :: t1) (s2 ++ x :: t2).
proof: Proof. by move=>*; apply: pperm_catL=>//; apply: permutation_skip. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)