Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ι → ο . ∀ x1 . (∀ x2 . wex (λ x3 . ∀ x4 . (∀ x5 . x0 x5 x4 x2)wceq (cv x4) (cv x3)))wex (λ x2 . ∀ x3 . wb (wcel (cv x3) (cv x2)) (wex (λ x4 . wa (wcel (cv x4) (cv x1)) (∀ x5 . x0 x5 x3 x4))))
as obj
-
as prop
aaf33..
theory
SetMM
stx
e4700..
address
TMLty..