Proofgold Term Root Disambiguation

(∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x2 = minus_SNo x3 ⟶ SNoLev x3 ∈ SNoLev x0 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0

as obj
-

as prop
1bfb9..

theory
HotG

stx
6bc83..

address
TMJYq..