Proofgold Object

λ x0 . and (struct_b_b_r_e_e x0) (unpack_b_b_r_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 : ι → ι → ο . λ x5 x6 . explicit_OrderedField x1 x5 x6 x2 x3 x4))

type
ι → ο

theory
HotG

name
OrderedFieldStruct

definition
PUa4W..

Megalodon
struct_b_b_r_e_e_ordered_field

proofgold address
TMWMk..^{struct_b_b_r_e_e_ordered_field}

creator
5731 Pr6Pc../619b3..

owner
5731 Pr6Pc../619b3..

term root
98aa9..