Proofgold Proposition

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

type
prop

theory
HoTg

name
ordinal_ind

proof
PUKG7..

Megalodon
-

proofgold address
TMF2w..

creator
2750 PrGxv../8392e..

owner
2750 PrGxv../8392e..

term root
bb557..