fact: Definition um_all2 (f1 f2 : U) := forall k, optionR P (find k f1) (find k f2).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)