proposition: Lemma fcatA (s1 s2 s3 : fmap) : disj s2 s3 -> fcat (fcat s1 s2) s3 = fcat s1 (fcat s2 s3).
proof: Proof. move=>H. elim/fmap_ind': s3 s1 s2 H=>[|k v s3 L IH] s1 s2 /=; first by rewrite !fcats0. rewrite disj_ins; case/andP=>H1 H2. by rewrite fcat_sins ?notin_path // IH // fcat_sins ?notin_path // fcat_sins. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)