Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0ordinal x1∀ x4 : ο . (PNoLt x0 x2 x1 x3x4)(x0 = x1PNoEq_ x0 x2 x3x4)(PNoLt x1 x3 x0 x2x4)x4
as obj
-
as prop
ebdc6..PNoLt_trichotomy_or_impred
theory
HF
stx
8964b..
address
TMNo4..PNoLt_trichotomy_or_impred