Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ SNoS_ omega ⟶ or (SNoL x0 = 0) (∃ x1 . SNo_max_of (SNoL x0) x1)

as obj
-

as prop
faaae..^{SNoS_omega_SNoL_max_exists}

theory
HotG

stx
2f9e1..