fact: Definition clone_morphism D f := let: Morphism _ fM := f return {type of @Morphism D for f} -> morphism_for D (Phant rT) in fun k => k fM.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)