Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_mult x0 x1 x2 x3)

as obj
4cad0..

as prop
-

theory
HoTg

stx
ddc14..

address
TMGRg..^{explicit_Nats_one_exp}