subgroup_product_laws

forall (G : Sort u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (group_args : @GroupLawArgs.{u} G one mul inv), forall (Hpred : forall (x : G), Prop), forall (N : forall (x : G), Prop), forall (h_args : @SubgroupLawArgs.{u} G one mul inv Hpred), forall (n_normal : @NormalSubgroupLawArgs.{u} G one mul inv N), @SubgroupLawArgs.{u} G one mul inv (@SubgroupProductPred.{u} G mul Hpred N)

fun G => fun one => fun mul => fun inv => fun group_args => fun Hpred => fun N => fun h_args => fun n_normal => fun (P : Prop) => fun (mk : forall (one_mem : @SubgroupProductPred.{u} G mul Hpred N one), forall (mul_closed : forall (a : G), forall (b : G), forall (ha : @SubgroupProductPred.{u} G mul Hpred N a), forall (hb : @SubgroupProductPred.{u} G mul Hpred N b), @SubgroupProductPred.{u} G mul Hpred N (mul a b)), forall (inv_closed : forall (a : G), forall (ha : @SubgroupProductPred.{u} G mul Hpred N a), @SubgroupProductPred.{u} G mul Hpred N (inv a)), P) => mk (@subgroup_product_one.{u} G one mul inv group_args Hpred N h_args (@normal_subgroup_laws.{u} G one mul inv N n_normal)) (@subgroup_product_mul_closed.{u} G one mul inv group_args Hpred N h_args n_normal) (@subgroup_product_inv_closed.{u} G one mul inv group_args Hpred N h_args n_normal)