Proofgold Proposition

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

type
prop

theory
HotG

name
ordinal_ind

proof
PUMB7..

Megalodon
ordinal_ind

proofgold address
TMHyu..^ordinal_ind

creator
4898 Pr6Pc../6c1d9..

owner
4898 Pr6Pc../6c1d9..

term root
bb557..