Proofgold Term Root Disambiguation

λ x0 . nat_primrec (field4 x0) (λ x1 x2 . field1b x0 x2 (RealsStruct_one x0))

as obj
8d1b1..^{RealsStruct_omega_embedding}

as prop
-

theory
HotG

stx
6b5ba..

address
TMFS8..^{RealsStruct_omega_embedding}