Proofgold Term Root Disambiguation

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

as obj
-

as prop
6fbb0..^{int_add_SNo_lem}

theory
HotG

stx
b160a..

address
TMLvP..^{int_add_SNo_lem}