proposition: Lemma pperm_in s1 s2 x : perm s1 s2 -> x \In s1 -> x \In s2.
proof: Proof. elim=>//??? =>[|?|_ I1 _ I2 /I1/I2]; rewrite ?InE; tauto. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)