Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ SNoLev (minus_SNo x1) ⊆ SNoLev x1

as obj
-

as prop
afc11..^{minus_SNo_Lev_lem1}

theory
HotG

stx
2cf07..

address
TMGTT..^{minus_SNo_Lev_lem1}