Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq choma (cmpt (λ x0 . ccat) (λ x0 . cmpt (λ x1 . cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)) (λ x1 . cxp (csn (cv x1)) (cfv (cv x1) (cfv (cv x0) chom)))))
as obj
-
as prop
12759..
theory
SetMM
stx
c36e5..
address
TMSo6..