Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cfae (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cuni (crn cmeas)) (λ x0 x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (co (cdm (cv x0)) (cuni (cdm (cv x1))) cmap)) (wcel (cv x3) (co (cdm (cv x0)) (cuni (cdm (cv x1))) cmap))) (wbr (crab (λ x4 . wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) (cv x0)) (λ x4 . cuni (cdm (cv x1)))) (cv x1) cae))))
as obj
-
as prop
81ff0..
theory
SetMM
stx
2e131..
address
TMTbU..