Proofgold Object

λ x0 x1 . and (subgroup x0 x1) (unpack_b_o x1 (λ x2 . λ x3 : ι → ι → ι . unpack_b_o x0 (λ x4 . λ x5 : ι → ι → ι . explicit_normal x2 x3 x4)))

type
ι → ι → ο

theory
HotG

name
normal_subgroup

definition
PUMaE..

Megalodon
normal_subgroup

proofgold address
TMUQx..^{normal_subgroup}

creator
4924 Pr6Pc../166f5..

owner
4924 Pr6Pc../166f5..

term root
071c7..