Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cfcf (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (crn cfil)) (λ x0 x1 . cmpt (λ x2 . co (cuni (cv x0)) (cuni (cv x1)) cmap) (λ x2 . co (cv x0) (cfv (cv x1) (co (cuni (cv x0)) (cv x2) cfm)) cfcls)))
as obj
-
as prop
9b664..
theory
SetMM
stx
8519a..
address
TMG8r..