Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ SNoS_ omega ⟶ or (SNoR x0 = 0) (∀ x1 : ο . (∀ x2 . SNo_min_of (SNoR x0) x2 ⟶ x1) ⟶ x1)

as obj
-

as prop
baaae..^{SNoS_omega_SNoR_min_exists}

theory
HotG

stx
2f9e1..

address
TMWy5..^{SNoS_omega_SNoR_min_exists}