fact: Definition pack := fun (bT : pcm) (b : PCM.mixin_of T) & phant_id (PCM.class bT) b => fun m => Pack (@Class T b m).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)