Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cgoq (cmpt2 (λ x0 x1 . com) (λ x0 x1 . com) (λ x0 x1 . csb (csuc (cun (cv x0) (cv x1))) (λ x2 . cgol (co (co (cv x2) (cv x0) cgoe) (co (cv x2) (cv x1) cgoe) cgob) (cv x2))))
as obj
-
as prop
fb167..
theory
SetMM
stx
d034f..
address
TMQfd..