Proofgold Term Root Disambiguation

∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 x3 . ∀ x4 : ι → ο . (∀ x5 . x5 ∈ PNo_bd x0 x1 ⟶ ∀ x6 : ι → ο . not (PNo_strict_imv x0 x1 x5 x6)) ⟶ x3 ∈ ordsucc x2 ⟶ PNo_strict_imv x0 x1 x3 x4 ⟶ not (x3 ∈ PNo_bd x0 x1)

as obj
-

as prop
33d61..^{Conj_PNo_bd_In__1__3}

theory
HotG

stx
202df..

address
TMNRB..^{Conj_PNo_bd_In__1__3}