Proofgold Object

λ x0 x1 x2 . ∀ x3 : ο . (∀ x4 . and (x4 ∈ RealsStruct_Npos x0) (field2b x0 x1 x4 = x2) ⟶ x3) ⟶ x3

type
ι → ι → ι → ο

theory
HotG

name
RealsStruct_divides

definition
PUVyd..

Megalodon
RealsStruct_divides

proofgold address
TMEjv..^{RealsStruct_divides}

creator
5857 Pr6Pc../14b71..

owner
5857 Pr6Pc../14b71..

term root
9b1a1..