Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ RealsStruct_one x0 = field4 x0 ⟶ ∀ x1 : ο . x1

as obj
-

as prop
52ab4..^{RealsStruct_one_neq_zero}

theory
HotG

stx
8f02a..

address
TMNKM..^{RealsStruct_one_neq_zero}