Proofgold Term Root Disambiguation

λ x0 x1 . If_i (x1 = 0) 0 (prim0 (λ x2 . and (CSNo x2) (mul_CSNo x2 x1 = x0)))

as obj
144bb..^div_CSNo

as prop
-

theory
HotG

stx
7edd8..

address
TMcjy..^div_CSNo