proposition: Lemma assocs_perm f1 f2 : valid (f1 \+ f2) -> perm (assocs (f1 \+ f2)) (assocs f1 ++ assocs f2).
proof: Proof. rewrite !pcmE /= !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. case: (UMC.from f1)=>//= g1 H1; case: (UMC.from f2)=>//= g2 H2. by case: ifP=>// D _; apply: seqof_fcat_perm D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)