Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ equip {x1 ∈ SNoS_ omega|SNoLev x1 = x0} (exp_SNo_nat 2 x0)

as obj
-

as prop
81ef7..^{SNoS_omega_Lev_equip}

theory
HotG

stx
2f9e1..

address
TMUgW..^{SNoS_omega_Lev_equip}