Proofgold Object

λ x0 . {x1 ∈ RealsStruct_N x0|x1 = field4 x0 ⟶ ∀ x2 : ο . x2}

type
ι → ι

theory
HotG

name
RealsStruct_Npos

definition
PUSVY..

Megalodon
RealsStruct_Npos

proofgold address
TMMXx..^{RealsStruct_Npos}

creator
5804 Pr6Pc../e1f46..

owner
5804 Pr6Pc../e1f46..

term root
18dcd..