Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 x7 . nat_primrec x1 (λ x8 . x3 (x4 (ap x6 x8) (explicit_Ring_with_id_exp_nat x0 x1 x2 x3 x4 x7 x8))) x5

as obj
a93ca..^{explicit_Ring_with_id_eval_poly}

as prop
-

theory
HotG

stx
30095..

address
TMJ6r..^{explicit_Ring_with_id_eval_poly}