Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (In x0 x1) (x0 = x1)) (In x1 x0)

as obj
-

as prop
3fa8b..^{ordinal_trichotomy_or}

theory
HF

stx
82de5..

address
TMNX9..^{ordinal_trichotomy_or}