Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ SNoEq_ (SNoLev x0) (SNo_extend0 x0) x0

as obj
-

as prop
12998..^{SNo_extend0_SNoEq}

theory
HotG

stx
fab7c..

address
TMcVb..^{SNo_extend0_SNoEq}