Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ x0 = pack_b_b_r_e_e (field0 x0) (field1b x0) (field2b x0) (RealsStruct_leq x0) (field4 x0) (RealsStruct_one x0)

as obj
-

as prop
f1cea..^{RealsStruct_eta}

theory
HotG

stx
8f02a..

address
TMWmf..^{RealsStruct_eta}