Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cinv (cmpt (λ x0 . ccat) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cin (co (cv x1) (cv x2) (cfv (cv x0) csect)) (ccnv (co (cv x2) (cv x1) (cfv (cv x0) csect))))))
as obj
-
as prop
81418..
theory
SetMM
stx
16f22..
address
TMZ3h..