Proofgold Object

λ x0 x1 . and (and (struct_b x1) (struct_b x0)) (unpack_b_o x1 (λ x2 . λ x3 : ι → ι → ι . unpack_b_o x0 (λ x4 . λ x5 : ι → ι → ι . and (and (x0 = pack_b x4 x3) (Group (pack_b x4 x3))) (x4 ⊆ x2))))

type
ι → ι → ο

theory
HotG

name
subgroup

definition
PUMaE..

Megalodon
subgroup

proofgold address
TMGMF..^subgroup

creator
4924 Pr6Pc../71dc5..

owner
4924 Pr6Pc../71dc5..

term root
994c6..