Proofgold Term Root Disambiguation

∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ PNo_bd x0 x1 ∈ ordsucc x2

as obj
-

as prop
4719e..^PNo_bd_In

theory
HotG

stx
9543e..

address
TMasN..^PNo_bd_In