subgroup_product_one

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 (S : forall (x : G), Prop), forall (T : forall (x : G), Prop), forall (s_args : @SubgroupLawArgs.{u} G one mul inv S), forall (t_args : @SubgroupLawArgs.{u} G one mul inv T), @SubgroupProductPred.{u} G mul S T one

fun G => fun one => fun mul => fun inv => fun group_args => fun S => fun T => fun s_args => fun t_args => @subgroup_product_intro.{u} G mul S T one one one (@subgroup_one.{u} G one mul inv S s_args) (@subgroup_one.{u} G one mul inv T t_args) (@group_one_mul.{u} G one mul inv group_args one)