fact: Definition axiom (f : U -> U') (mfunc : K * V -> option V') := f =1 omap mfunc.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)