Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . ordinal x0 ⟶ PNoEq_ x0 x1 (λ x4 . or (x1 x4) (x4 = x0)) ⟶ x3 ∈ x0 ⟶ PNoEq_ x3 (λ x4 . or (x1 x4) (x4 = x0)) x2 ⟶ ordinal x3 ⟶ PNoLt x3 x2 x0 x1 ⟶ not (PNoLt x0 x1 x3 x2)

as obj
-

as prop
e1d83..^{Conj_PNo_rel_imv_ex__7__4}

theory
HotG

stx
b740c..

address
TMZAY..^{Conj_PNo_rel_imv_ex__7__4}