Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cflf (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)) cflim)))
as obj
-
as prop
1eb38..
theory
SetMM
stx
8519a..
address
TMQxu..