Proofgold Term Root Disambiguation

λ x0 x1 x2 x3 . nat_primrec (field3 x0) (λ x4 . field1b x0 (field2b x0 (ap x2 x4) (CRing_with_id_omega_exp x0 x3 x4))) x1

as obj
808af..^{CRing_eval_poly}

as prop
-

theory
HotG

stx
339e9..

address
TMUwU..^{CRing_eval_poly}