NormalSetoid

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 (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), @Setoid.{u} G

fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => @Setoid.mk.{u} G (@NormalRel.{succ u} G one mul inv N) (fun (P : Prop) => fun (mk_equiv : forall (refl_arg : forall (x : G), @NormalRel.{succ u} G one mul inv N x x), forall (symm_arg : forall (x : G), forall (y : G), forall (p : @NormalRel.{succ u} G one mul inv N x y), @NormalRel.{succ u} G one mul inv N y x), forall (trans_arg : forall (x : G), forall (y : G), forall (z : G), forall (p : @NormalRel.{succ u} G one mul inv N x y), forall (q : @NormalRel.{succ u} G one mul inv N y z), @NormalRel.{succ u} G one mul inv N x z), P) => mk_equiv (@normal_rel_refl.{succ u} G one mul inv group_args N normal_args) (@normal_rel_symm.{succ u} G one mul inv group_args N normal_args) (@normal_rel_trans.{succ u} G one mul inv group_args N normal_args))