Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ add_SNo (ordsucc x0) x2 = ordsucc (add_SNo x0 x2)) ⟶ SNo x0 ⟶ SNo x1 ⟶ ordinal (add_SNo x0 x1) ⟶ ordinal (ordsucc x0) ⟶ SNo (ordsucc x0) ⟶ add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1)

as obj
-

as prop
4d514..^{Conj_add_SNo_ordinal_SL__14__0}

theory
HotG

stx
202df..

address
TMP4F..^{Conj_add_SNo_ordinal_SL__14__0}