fact: Definition clone_pmap (F : object_map) := fun (funF : map) & phant_id (apply funF) F => fun (pfunF0 : pmap) & phant_id (apply pfunF0) F => fun Fher (pfunF := @Pmap funF Fher) & phant_id pfunF0 pfunF => pfunF.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)