Proofgold Proposition

∀ x0 : ι → ο . (∀ x1 . nat_p x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1

type
prop

theory
HotG

name
nat_complete_ind

proof
PUL8Q..

Megalodon
nat_complete_ind

proofgold address
TMSj9..^{nat_complete_ind}

creator
4882 Pr6Pc../8edc3..

owner
4882 Pr6Pc../8edc3..

term root
d32e5..