Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq csubma (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cmpt2 (λ x5 x6 . cdif (cv x0) (csn (cv x3))) (λ x5 x6 . cdif (cv x0) (csn (cv x4))) (λ x5 x6 . co (cv x5) (cv x6) (cv x2))))))
as obj
-
as prop
32eec..
theory
SetMM
stx
9fb9c..
address
TMWVb..