Proofgold Object

λ x0 x1 x2 . and (RealsStruct_leq x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)

type
ι → ι → ι → ο

theory
HotG

name
RealsStruct_lt

definition
PUVyd..

Megalodon
RealsStruct_lt

proofgold address
TMcan..^{RealsStruct_lt}

creator
5857 Pr6Pc../3768f..

owner
5857 Pr6Pc../3768f..

term root
3a46d..