Proofgold Term Root Disambiguation

∀ x0 x1 . TransSet x0 ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ SNoS_ x2 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3) ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNoCutP (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo) ⟶ SNoLev (minus_SNo x1) ⊆ SNoLev x1

as obj
-

as prop
49f1d..^{Conj_minus_SNo_Lev_lem1__22__2}

theory
HotG

stx
202df..

address
TMYiE..^{Conj_minus_SNo_Lev_lem1__22__2}