proposition: Lemma pperm_cons x s1 s2 : perm (x :: s1) (x :: s2) <-> perm s1 s2.
proof: Proof. by split; [apply/(@pperm_cat_consR [::] [::]) | apply: permutation_skip]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)