proposition: Lemma seqof_fcat_perm s1 s2 : disj s1 s2 -> perm (seq_of (fcat s1 s2)) (seq_of s1 ++ seq_of s2).
proof: Proof. elim/fmap_ind': s2 s1=>[|k v s L IH] s1. - by rewrite fcats0 cats0. rewrite fcat_sins disj_ins; case/andP=>D1 D2. apply: pperm_trans (seqof_ins_perm _ _) _. - by rewrite supp_fcat inE /= negb_or D1 (notin_path L). move/(pperm_cons (k, v))/pperm_trans: {IH} (IH _ D2); apply. apply: pperm_trans (pperm_cons_catCA _ _ _) _; apply: pperm_catL=>//. by apply/pperm_sym; apply: seqof_ins_perm (notin_path L). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)