proposition: Lemma disj_fcat (s s1 s2 : fmap) : disj s (fcat s1 s2) = disj s s1 && disj s s2.
proof: Proof. elim/fmap_ind': s s1 s2=>[|k v s L IH] s1 s2. - by rewrite !(disjC nil) !disj_nil. rewrite !(disjC (ins _ _ _)) !disj_ins supp_fcat inE /= negb_or. case: (k \in supp s1)=>//=. case: (k \in supp s2)=>//=; first by rewrite andbF. by rewrite -!(disjC s) IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)