Proofgold Object

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

type
ι → ι → ι → ι → ο

theory
HotG

name
-

definition
PUSkV..

Megalodon
-

proofgold address
TMGyU..

creator
5784 Pr6Pc../c63e4..

owner
5784 Pr6Pc../c63e4..

term root
4e65b..