proposition: Lemma all_supp_fcatP : all C (supp f) -> all C (supp g) -> all C (supp (fcat f g)).
proof: Proof. move=>H1 H2; apply/allP=>x; rewrite supp_fcat inE /=. by case/orP; [move/(allP H1) | move/(allP H2)]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)