Proofgold Proposition

PNo_downc = λ x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . ∃ x4 . and (ordinal x4) (∃ x6 : ι → ο . and (x1 x4 x6) (PNoLe x2 x3 x4 x6))

type
prop

theory
hf axiom

name
-

proof
-

Megalodon
PNo_downc_def

proofgold address
-

creator

owner

term root
11997..