fact: Definition subpcm_mixin : SubPCM.mixin_of D (base class) := @SubPCM.Mixin V D cT (TPCM.base (base class)) subtpcm_struct.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)