Proofgold Term Root Disambiguation

∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2

as obj
-

as prop
b4776..^{ordsuccE_impred}

theory
HF

stx
0d78c..

address
TMZHC..^{ordsuccE_impred}