Proofgold Term Root Disambiguation

λ x0 . nat_primrec 0 (λ x1 x2 . If_i (ordsucc x2 ∈ x0) (ordsucc x2) 0)

as obj
96eca..

as prop
-

theory
HotG

stx
33c6f..

address
TMV86..