Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cscaf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cfv (cv x0) csca) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cv x2) (cfv (cv x0) cvsca))))
as obj
-
as prop
56a33..
theory
SetMM
stx
257fe..
address
TMNJf..