proposition: Lemma pperm_cons_catCA s1 s2 x : perm (x :: s1 ++ s2) (s1 ++ x :: s2).
proof: Proof. rewrite -cat1s -(cat1s _ s2) !catA. by apply/pperm_cat2rL/pperm_catC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)