Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cref (copab (λ x0 x1 . wa (wceq (cuni (cv x1)) (cuni (cv x0))) (wral (λ x2 . wrex (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cv x1)) (λ x2 . cv x0))))
as obj
-
as prop
4b848..
theory
SetMM
stx
ec0d9..
address
TMFx6..