Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 : ι → ο . (∀ x3 . nat_p x3 ⟶ x0 = ordsucc x3 ⟶ x2 (ordsucc x3)) ⟶ x2 x0

type
prop

theory
HF

name
-

proof
PUZkx..

Megalodon
pos_nat_inv_impred

proofgold address
TMKL2..^{pos_nat_inv_impred}

creator
2364 PrGxv../022d7..

owner
2364 PrGxv../022d7..

term root
848c2..