Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 : ι → ι . nat_primrec 4a7ef.. (λ x3 x4 . If_i (prim1 x3 x0) 4a7ef.. (e37c0.. (x2 x3) x4)) (4ae4a.. x1)

as obj
5fbd5..

as prop
-

theory
HoTg

stx
1ad4e..

address
TMHds..