Proofgold Term Root Disambiguation

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ add_SNo (minus_SNo x3) x3 = 0) ⟶ SNo (minus_SNo x0) ⟶ x1 = add_SNo (minus_SNo x0) x2 ⟶ SNo x2 ⟶ SNoLt x2 x0 ⟶ SNo (minus_SNo x2) ⟶ SNoLt x1 0

as obj
-

as prop
6cfb5..^{Conj_add_SNo_minus_SNo_linv__9__5}

theory
HotG

stx
b740c..

address
TMLkP..^{Conj_add_SNo_minus_SNo_linv__9__5}