Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 . nat_primrec x2 (λ x6 . x4 x5)

as obj
77341..

as prop
-

theory
HoTg

stx
32977..

address
TMH1F..^{explicit_Ring_exp_nat}