Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cphtpc (cmpt (λ x0 . ctop) (λ x0 . copab (λ x1 x2 . wa (wss (cpr (cv x1) (cv x2)) (co cii (cv x0) ccn)) (wne (co (cv x1) (cv x2) (cfv (cv x0) cphtpy)) c0))))
as obj
-
as prop
c1362..
theory
SetMM
stx
bc3a6..
address
TMMEm..