Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cbc (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cz) (λ x0 x1 . cif (wcel (cv x1) (co cc0 (cv x0) cfz)) (co (cfv (cv x0) cfa) (co (cfv (co (cv x0) (cv x1) cmin) cfa) (cfv (cv x1) cfa) cmul) cdiv) cc0))
as obj
-
as prop
b11d9..
theory
SetMM
stx
33c8c..
address
TMZ8s..