proposition: Lemma gFunctorI gT (G H : {group gT}) : F gT G :&: H = F gT G :&: F gT (G :&: H).
proof: Proof. rewrite -{1}(setIidPr (gFsub F G)) setIAC setIC. rewrite -(setIidPr (gFhereditary (subsetIl G H))). by rewrite setIC -setIA (setIidPr (gFsub F (G :&: H))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)