Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . ordinal x0PNoEq_ x0 (λ x4 . and (x1 x4) (x4 = x0∀ x5 : ο . x5)) x1PNoEq_ x3 x2 (λ x4 . and (x1 x4) (x4 = x0∀ x5 : ο . x5))and (x1 x3) (x3 = x0∀ x4 : ο . x4)ordinal x3PNoLt x0 x1 x3 x2not (PNoLt x3 x2 x0 x1)
as obj
-
as prop
ec2d3..Conj_PNo_rel_imv_ex__16__2
theory
HotG
stx
b740c..
address
TMReG..Conj_PNo_rel_imv_ex__16__2