third_iso_hn_conj_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 (gq : @ThirdIsoGN.{u} G one mul inv N group_args n_normal), forall (nq : @ThirdIsoGN.{u} G one mul inv N group_args n_normal), forall (hnq : @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal nq), @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal gq nq) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal gq))

fun G => fun one => fun mul => fun inv => fun N => fun Hpred => fun group_args => fun n_normal => fun h_normal => @Quotient.indProp.{u} G (@NormalSetoid.{u} G one mul inv N group_args n_normal) (fun (gq : @NormalQuot.{u} G one mul inv N group_args n_normal) => forall (nq : @ThirdIsoGN.{u} G one mul inv N group_args n_normal), forall (hnq : @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal nq), @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal gq nq) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal gq))) (fun (g : G) => fun (nq : @ThirdIsoGN.{u} G one mul inv N group_args n_normal) => fun (hnq : @ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal nq) => hnq (@ThirdIsoHNPred.{u} G one mul inv N Hpred group_args n_normal (@ThirdIsoGNMul.{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 g) nq) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g)))) (fun (h : G) => fun (hh : Hpred h) => fun (eqh : @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 h) nq) => @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 (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g) nq) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g))) (mul (mul g h) (inv g)) (@normal_conj_closed.{succ u} G one mul inv Hpred h_normal g h hh) (@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 (mul g h) (inv g))) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal (mul g h)) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (inv g))) (@ThirdIsoGNMul.{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 g) nq) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g))) (@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 (mul g h)) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (inv g))) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (mul (mul g h) (inv g))) (@normal_quot_mul_mk.{u} G one mul inv N group_args n_normal (mul g h) (inv g))) (@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 (mul g h)) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g) nq) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (inv g)) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g)) (@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 g h)) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g) (@NormalQuotMk.{u} G one mul inv N group_args n_normal h)) (@ThirdIsoGNMul.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g) nq) (@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 g) (@NormalQuotMk.{u} G one mul inv N group_args n_normal h)) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (mul g h)) (@normal_quot_mul_mk.{u} G one mul inv N group_args n_normal g h)) (@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 g) (@NormalQuotMk.{u} G one mul inv N group_args n_normal g) (@NormalQuotMk.{u} G one mul inv N group_args n_normal h) nq (@Eq.refl.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotMk.{u} G one mul inv N group_args n_normal g)) eqh)) (@eq_symm.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@ThirdIsoGNInv.{u} G one mul inv N group_args n_normal (@NormalQuotMk.{u} G one mul inv N group_args n_normal g)) (@NormalQuotMk.{u} G one mul inv N group_args n_normal (inv g)) (@normal_quot_inv_mk.{u} G one mul inv N group_args n_normal g))))))