Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cocv (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x0) cip)) (cfv (cfv (cv x0) csca) c0g)) (λ x3 . cv x1)) (λ x2 . cfv (cv x0) cbs))))
as obj
-
as prop
397fc..
theory
SetMM
stx
ea284..
address
TMX8s..