proposition: Lemma un_nullP : null \notin supp f -> null \notin supp g -> null \notin supp (fcat f g).
proof: Proof. by move=>H1 H2; rewrite supp_fcat negb_or H1 H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)