Proofgold Term Root Disambiguation

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

as obj
1319b..

as prop
-

theory
HotG

stx
f6bb3..

address
TMbhJ..