Proofgold Term Root Disambiguation

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

as obj
-

as prop
0dfd1..^{SNo_extend0_nIn}

theory
HotG

stx
fab7c..

address
TMda5..^{SNo_extend0_nIn}