third_iso_hn_mul_closed

forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv Hpred), forall (q1 : @ThirdIsoGN.{u} G one mul inv N group_args n_normal), forall (q2 : @ThirdIsoGN.{u} G one mul inv N group_args n_normal), forall (hq1 : @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal q1), forall (hq2 : @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal q2), @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal q1 q2)

fun G => fun one => fun mul => fun inv => fun N => fun Hpred => fun group_args => fun n_normal => fun h_normal => fun q1 => fun q2 => fun hq1 => fun hq2 => hq1 (@ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal q1 q2)) (fun (a : G) => fun (ha : Hpred a) => fun (eqa : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotMk.{u} G one mul inv N group_args n_normal a) q1) => hq2 (@ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal q1 q2)) (fun (b : G) => fun (hb : Hpred b) => fun (eqb : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotMk.{u} G one mul inv N group_args n_normal b) q2) => @third_iso_hn_intro.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal q1 q2) (mul a b) (@subgroup_mul_closed.{succ u} G one mul inv Hpred (@normal_subgroup_laws.{succ u} G one mul inv Hpred h_normal) a b ha hb) (@eq_trans.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (mul a b)) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal a) (@NormalQuotMk.{u} G one mul inv N group_args n_normal b)) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal q1 q2) (@eq_symm.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal a) (@NormalQuotMk.{u} G one mul inv N group_args n_normal b)) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (mul a b)) (@normal_quot_mul_mk.{u} G one mul inv N group_args n_normal a b)) (@eq_congr2.{succ u,succ u,succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuot.{u} G one mul inv N group_args n_normal) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal) (@NormalQuotMk.{u} G one mul inv N group_args n_normal a) q1 (@NormalQuotMk.{u} G one mul inv N group_args n_normal b) q2 eqa eqb))))