Proofgold Term Root Disambiguation

(∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo (minus_SNo x0) ⟶ add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1 ⟶ x1 = x2) ⟶ ∀ x0 : ο . x0

as obj
-

as prop
67c81..

theory
HotG

stx
6bc83..

address
TMMZH..