fact: Definition clone (F : object_map) := fun isoF & phant_id (apply isoF) F => fun (funF0 : map) & phant_id (apply funF0) F => fun Fcont (funF := @Map isoF Fcont) & phant_id funF0 funF => funF.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)