Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq ccmtN (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (cfv (cv x0) cbs)) (wceq (cv x1) (co (co (cv x1) (cv x2) (cfv (cv x0) cmee)) (co (cv x1) (cfv (cv x2) (cfv (cv x0) coc)) (cfv (cv x0) cmee)) (cfv (cv x0) cjn))))))
as obj
-
as prop
80613..
theory
SetMM
stx
7eb09..
address
TMGmv..