Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq clcmf (cmpt (λ x0 . cpw cz) (λ x0 . cif (wcel cc0 (cv x0)) cc0 (cinf (crab (λ x1 . wral (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cv x0)) (λ x1 . cn)) cr clt)))
as obj
-
as prop
cff71..
theory
SetMM
stx
0aa70..
address
TMGKU..