Proofgold Term Root Disambiguation

λ x0 x1 . If_i (x1 = 0) 0 (prim0 (λ x2 . and (SNo x2) (mul_SNo x2 x1 = x0)))

as obj
41b02..^div_SNo

as prop
-

theory
HotG

stx
7edd8..

address
TMJtK..^div_SNo