Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ field2b x0 (Field_minus (Field_of_RealsStruct x0) (RealsStruct_one x0)) (Field_minus (Field_of_RealsStruct x0) (RealsStruct_one x0)) = RealsStruct_one x0

as obj
-

as prop
701ed..^{RealsStruct_minus_one_square}

theory
HotG

stx
56719..

address
TMPnE..^{RealsStruct_minus_one_square}