proposition: Lemma supp_fcat s1 s2 : supp (fcat s1 s2) =i [predU supp s1 & supp s2].
proof: Proof. elim/fmap_ind': s2 s1=>[|k v s L IH] s1. - by rewrite supp_nil fcats0 => x; rewrite inE /= orbF. rewrite fcat_sins ?notin_path // => x. rewrite supp_ins !inE /=. case E: (x == k)=>/=. - by rewrite supp_ins inE /= E orbT. by rewrite IH supp_ins inE /= inE /= E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)