fact: Definition union f1 f2 := if (f1, f2) is (Def fs1 pf1, Def fs2 pf2) then if disj fs1 fs2 then Def (all_supp_fcatP pf1 pf2) else Undef else Undef.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)