proposition: Lemma pperm_map A B (f : A -> B) (s1 s2 : seq A) : perm s1 s2 -> perm (map f s1) (map f s2).
proof: Proof. elim=>[//|||??? _ IH1 _ IH2]*; by [apply/pperm_cons | apply/permutation_swap | apply/(pperm_trans IH1 IH2)]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)