Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cwun (cab (λ x0 . w3a (wtr (cv x0)) (wne (cv x0) c0) (wral (λ x1 . w3a (wcel (cuni (cv x1)) (cv x0)) (wcel (cpw (cv x1)) (cv x0)) (wral (λ x2 . wcel (cpr (cv x1) (cv x2)) (cv x0)) (λ x2 . cv x0))) (λ x1 . cv x0))))
as obj
-
as prop
7c217..
theory
SetMM
stx
c8ab1..
address
TMJP9..