Proofgold Proposition

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

type
prop

theory
HF

name
-

proof
PUZkx..

Megalodon
nat_inv_impred

proofgold address
TMdgZ..^{nat_inv_impred}

creator
2364 PrGxv../efc95..

owner
2364 PrGxv../efc95..

term root
dfa3c..