Proofgold Term Root Disambiguation

λ x0 . f482f.. (nat_primrec (0fc90.. 48ef8.. (λ x1 . If_i (x1 = 4a7ef..) (4ae4a.. 4a7ef..) 4a7ef..)) (λ x1 x2 . 0fc90.. 48ef8.. (λ x3 . If_i (x3 = 4a7ef..) (4ae4a.. 4a7ef..) (616bf.. (f482f.. x2 (prim3 x3)) (f482f.. x2 x3)))) x0)

as obj
455bd..

as prop
-

theory
HoTg

stx
f96db..

address
TMbiB..