Proofgold Term Root Disambiguation

∀ x0 x1 . In x0 x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x0 x2 x3 ⟶ not (x2 x0) ⟶ x3 x0 ⟶ PNoLt_ x1 x2 x3

as obj
-

as prop
e7258..^PNoLt__I

theory
HF

stx
8964b..

address
TMTWs..^PNoLt__I