Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cumgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (crab (λ x3 . wceq (cfv (cv x3) chash) c2) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx)))
as obj
-
as prop
a4408..
theory
SetMM
stx
fb3f6..
address
TMVqJ..