Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cpautN (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wf1o (cfv (cv x0) cpsubsp) (cfv (cv x0) cpsubsp) (cv x1)) (wral (λ x2 . wral (λ x3 . wb (wss (cv x2) (cv x3)) (wss (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)))) (λ x3 . cfv (cv x0) cpsubsp)) (λ x2 . cfv (cv x0) cpsubsp)))))
as obj
-
as prop
0b283..
theory
SetMM
stx
c5cfe..
address
TMH5K..