Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ο . wceq (cofc x0) (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cdm (cv x1)) (λ x3 . co (cfv (cv x3) (cv x1)) (cv x2) x0)))
as obj
-
as prop
46765..
theory
SetMM
stx
2758d..
address
TMPB4..