Proofgold Proposition

∀ 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)

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_PNo_bd_In__1__3

proofgold address
TMSNN..^{Conj_PNo_bd_In__1__3}

creator
35045 PrNpY../82a12..

owner
35047 PrNpY../200fe..

term root
75a88..