Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cfbas (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . w3a (wne (cv x1) c0) (wnel c0 (cv x1)) (wral (λ x2 . wral (λ x3 . wne (cin (cv x1) (cpw (cin (cv x2) (cv x3)))) c0) (λ x3 . cv x1)) (λ x2 . cv x1))) (λ x1 . cpw (cpw (cv x0)))))
as obj
-
as prop
e3015..
theory
SetMM
stx
ea284..
address
TMHQY..