Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cmpps (cmpt (λ x0 . cvv) (λ x0 . coprab (λ x1 x2 x3 . wa (wcel (cotp (cv x1) (cv x2) (cv x3)) (cfv (cv x0) cmpst)) (wcel (cv x3) (co (cv x1) (cv x2) (cfv (cv x0) cmcls))))))
as obj
-
as prop
f44db..
theory
SetMM
stx
74203..
address
TMKZY..