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