Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x1) (cxp (cv x0) (cv x0)) cfrlm) (cop (cfv cnx cmulr) (co (cv x1) (cotp (cv x0) (cv x0) (cv x0)) cmmul)) csts))
as obj
-
as prop
415e0..
theory
SetMM
stx
9fb9c..
address
TMEyR..