proposition: Lemma pmorphimF : GFunctor.pcontinuous F.
proof: Proof. move=> gT rT G D f; rewrite -morphimIdom -(setIidPl (gFsub F G)) setICA. apply: (subset_trans (morphimS f (gFhereditary (subsetIr D G)))). by rewrite (subset_trans (morphimF F _ _ )) ?morphimIdom ?subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)