Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (f0c46.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10(x1 = x11∀ x13 : ο . x13)(x2 = x11∀ x13 : ο . x13)(x3 = x11∀ x13 : ο . x13)(x4 = x11∀ x13 : ο . x13)(x5 = x11∀ x13 : ο . x13)(x6 = x11∀ x13 : ο . x13)(x7 = x11∀ x13 : ο . x13)(x8 = x11∀ x13 : ο . x13)(x9 = x11∀ x13 : ο . x13)(x10 = x11∀ x13 : ο . x13)not (x0 x1 x11)x0 x2 x11not (x0 x3 x11)not (x0 x4 x11)x0 x5 x11not (x0 x6 x11)not (x0 x7 x11)x0 x8 x11not (x0 x9 x11)x0 x10 x11x12)x12
as obj
6a2f1..
as prop
-
theory
HotG
stx
2906e..
address
TMbnZ..