Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq ccusp (crab (λ x0 . wral (λ x1 . wcel (cv x1) (cfv (cfv (cv x0) cuss) ccfilu)wne (co (cfv (cv x0) ctopn) (cv x1) cflim) c0) (λ x1 . cfv (cfv (cv x0) cbs) cfil)) (λ x0 . cusp))
as obj
-
as prop
a4882..
theory
SetMM
stx
e06a4..
address
TMbnr..