fact: Record mixin_of (f : U -> U') := Mixin { mfunc : K * V -> option V'; _ : axiom f mfunc}.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)