Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cgi (cmpt (λ x0 . cvv) (λ x0 . crio (λ 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 . crn (cv x0))) (λ x1 . crn (cv x0))))
as obj
-
as prop
949f9..
theory
SetMM
stx
d4238..
address
TMQPL..