Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2)x1)x1)∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . In x3 x2not (x0 x3))x1)x1
as obj
-
as prop
48a85..least_ordinal_ex
theory
HF
stx
82de5..
address
TMUkN..least_ordinal_ex