Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cnrm (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wss (cv x2) (cv x3)) (wss (cfv (cv x3) (cfv (cv x0) ccl)) (cv x1))) (λ x3 . cv x0)) (λ x2 . cin (cfv (cv x0) ccld) (cpw (cv x1)))) (λ x1 . cv x0)) (λ x0 . ctop))
as obj
-
as prop
d36db..
theory
SetMM
stx
1b7b9..
address
TMYmg..