Proofgold Object

λ x0 . decode_r (ap x0 3)

type
ι → ι → ι → ο

theory
HotG

name
RealsStruct_leq

definition
PUSkV..

Megalodon
RealsStruct_leq

proofgold address
TMGzX..^{RealsStruct_leq}

creator
5784 Pr6Pc../9a0fd..

owner
5784 Pr6Pc../9a0fd..

term root
e5950..