Proofgold Object

λ x0 x1 x2 x3 . unpack_b_o x0 (λ x4 . λ x5 : ι → ι → ι . and (and (x2 ∈ x4) (x3 ∈ x4)) (x5 x2 (explicit_Group_inverse x4 x5 x3) ∈ ap x1 0))

type
ι → ι → ι → ι → ο

theory
HotG

name
normal_subgroup_equiv

definition
PUMaE..

Megalodon
normal_subgroup_equiv

proofgold address
TMHp4..^{normal_subgroup_equiv}

creator
4924 Pr6Pc../30ae4..

owner
4924 Pr6Pc../30ae4..

term root
8d6a0..