Proofgold Object

λ x0 . λ x1 : ι → ι → ι . λ x2 . and (Group (pack_b x2 x1)) (x2 ⊆ x0)

type
ι → (ι → ι → ι) → ι → ο

theory
HotG

name
explicit_subgroup

definition
PUMaE..

Megalodon
explicit_subgroup

proofgold address
TMUKd..^{explicit_subgroup}

creator
4924 Pr6Pc../cc265..

owner
4924 Pr6Pc../cc265..

term root
4f273..