Proofgold Proposition

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ explicit_Nats {x6 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x6 = x1 ⟶ ∀ x7 : ο . x7} x2 (λ x6 . x3 x6 x2)

type
prop

theory
HotG

name
explicit_PosNats_natOfOrderedField

proof
PUa4W..

Megalodon
explicit_PosNats_natOfOrderedField

proofgold address
TMZEM..^{explicit_PosNats_natOfOrderedField}

creator
5731 Pr6Pc../bcdc4..

owner
5731 Pr6Pc../bcdc4..

term root
36987..