Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq csubgr (copab (λ x0 x1 . w3a (wss (cfv (cv x0) cvtx) (cfv (cv x1) cvtx)) (wceq (cfv (cv x0) ciedg) (cres (cfv (cv x1) ciedg) (cdm (cfv (cv x0) ciedg)))) (wss (cfv (cv x0) cedg) (cpw (cfv (cv x0) cvtx)))))
as obj
-
as prop
e7747..
theory
SetMM
stx
fb3f6..
address
TMPFJ..