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