Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq crqp (cmpt (λ x0 . cprime) (λ x0 . cin ceqp (csb (crab (λ x1 . wrex (λ x2 . wss (cima (ccnv (cv x1)) (cdif cz (csn cc0))) (cv x2)) (λ x2 . crn cuz)) (λ x1 . co cz cz cmap)) (λ x1 . cxp (cv x1) (cin (cv x1) (co cz (co cc0 (co (cv x0) c1 cmin) cfz) cmap))))))
as obj
-
as prop
c8f2d..
theory
SetMM
stx
a24a7..
address
TMVgz..