Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cexid (cab (λ x0 . wrex (λ x1 . wral (λ x2 . wa (wceq (co (cv x1) (cv x2) (cv x0)) (cv x2)) (wceq (co (cv x2) (cv x1) (cv x0)) (cv x2))) (λ x2 . cdm (cdm (cv x0)))) (λ x1 . cdm (cdm (cv x0)))))
as obj
-
as prop
01357..
theory
SetMM
stx
eb63f..
address
TMQPK..