proposition: Lemma fcatsK (s s1 s2 : fmap) : disj s1 s && disj s2 s -> fcat s1 s = fcat s2 s -> s1 = s2.
proof: Proof. elim/fmap_ind': s s1 s2=>// k v s. move/notin_path=>H IH s1 s2; rewrite !disj_ins. case/andP; case/andP=>H1 H2; case/andP=>H3 H4. rewrite !fcat_sins // => H5. apply: IH; first by rewrite H2 H4. by apply: cancel_ins H5; rewrite supp_fcat negb_or /= ?H1?H3 H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)