Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cusp (cab (λ x0 . wa (wcel (cfv (cv x0) cuss) (cfv (cfv (cv x0) cbs) cust)) (wceq (cfv (cv x0) ctopn) (cfv (cfv (cv x0) cuss) cutop))))
as obj
-
as prop
969d1..
theory
SetMM
stx
e06a4..
address
TMMMf..