Proofgold Term Root Disambiguation

λ x0 x1 . nat_primrec (field4 x0) (λ x2 . field2b x0 x1)

as obj
5d354..^{CRing_with_id_omega_exp}

as prop
-

theory
HotG

stx
339e9..

address
TMQDS..^{CRing_with_id_omega_exp}