Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3(∀ x4 . x4x0SNoLt x4 (SNoCut x2 x3))(∀ x4 . x4x1SNoLt (SNoCut x2 x3) x4)(∀ x4 . x4x2SNoLt x4 (SNoCut x0 x1))(∀ x4 . x4x3SNoLt (SNoCut x0 x1) x4)SNoCut x0 x1 = SNoCut x2 x3
as obj
-
as prop
f6661..SNoCut_ext
theory
HotG
stx
fab7c..
address
TMQED..SNoCut_ext