Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ο . wceq (cofr x0) (copab (λ x1 x2 . wral (λ x3 . wbr (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) x0) (λ x3 . cin (cdm (cv x1)) (cdm (cv x2)))))
as obj
-
as prop
c51f0..
theory
SetMM
stx
3c2bc..
address
TMWxx..