Proofgold Proposition

∀ x0 . explicit_Group {x1 ∈ setexp x0 x0|bij x0 x0 (ap x1)} (λ x1 x2 . lam x0 (λ x3 . ap x2 (ap x1 x3)))

type
prop

theory
HotG

name
explicit_Group_symgroup

proof
PUMaE..

Megalodon
explicit_Group_symgroup

proofgold address
TMUju..^{explicit_Group_symgroup}

creator
4924 Pr6Pc../7f088..

owner
4924 Pr6Pc../7f088..

term root
75533..