Proofgold Object

λ x0 x1 . ∀ x2 . x2 ∈ prim3 x1 ⟶ or (ordinal x2) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = Sing x4) ⟶ x3) ⟶ x3)

type
ι → ι → ο

theory
HotG

name
ExtendedSNoElt_

definition
PUQvq..

Megalodon
ExtendedSNoElt_

proofgold address
TMRQw..^{ExtendedSNoElt_}

creator
28444 PrQUS../47c73..

owner
28444 PrQUS../47c73..

term root
13321..