Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ∀ x1 : ο . (∀ x2 x3 . SNoCutP x2 x3 ⟶ (∀ x4 . x4 ∈ x2 ⟶ SNoLev x4 ∈ SNoLev x0) ⟶ (∀ x4 . x4 ∈ x3 ⟶ SNoLev x4 ∈ SNoLev x0) ⟶ x0 = SNoCut x2 x3 ⟶ x1) ⟶ x1

as obj
-

as prop
109f1..^SNo_etaE

theory
HotG

stx
fab7c..

address
TMMaN..^SNo_etaE