Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cida (cmpt (λ x0 . ccat) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cotp (cv x1) (cv x1) (cfv (cv x1) (cfv (cv x0) ccid)))))
as obj
-
as prop
88cc2..
theory
SetMM
stx
c36e5..
address
TMKyt..