Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cina (cab (λ x0 . w3a (wne (cv x0) c0) (wceq (cfv (cv x0) ccf) (cv x0)) (wral (λ x1 . wbr (cpw (cv x1)) (cv x0) csdm) (λ x1 . cv x0))))
as obj
-
as prop
28913..
theory
SetMM
stx
c8ab1..
address
TMEnb..