fact: Record mixin_of (T : Type) (base : PCM.mixin_of T) (U := PCM T base) : Type := Mixin {subpcm_struct_op : subpcm_st U V D}.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)