Proofgold Term Root Disambiguation

∀ x0 x1 . x1 ∈ omega ⟶ ∀ x2 . nat_p x2 ⟶ x0 ∈ add_SNo x1 x2 ⟶ or (x0 ∈ x1) (add_SNo x0 (minus_SNo x1) ∈ x2)

as obj
-

as prop
584cf..^{add_SNo_omega_In_cases}

theory
HotG

stx
2f9e1..

address
TMT8F..^{add_SNo_omega_In_cases}