Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cplr (coprab (λ x0 x1 x2 . wa (wa (wcel (cv x0) cnr) (wcel (cv x1) cnr)) (wex (λ x3 . wex (λ x4 . wex (λ x5 . wex (λ x6 . wa (wa (wceq (cv x0) (cec (cop (cv x3) (cv x4)) cer)) (wceq (cv x1) (cec (cop (cv x5) (cv x6)) cer))) (wceq (cv x2) (cec (cop (co (cv x3) (cv x5) cpp) (co (cv x4) (cv x6) cpp)) cer)))))))))
as obj
-
as prop
45291..
theory
SetMM
stx
338b7..
address
TMbpz..