Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq chod (cmpt2 (λ x0 x1 . co chil chil cmap) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cmv)))
as obj
-
as prop
06172..
theory
SetMM
stx
337cc..
address
TMPKY..