Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cqg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (cfv (cv x0) cbs)) (wcel (co (cfv (cv x2) (cfv (cv x0) cminusg)) (cv x3) (cfv (cv x0) cplusg)) (cv x1)))))
as obj
-
as prop
464e8..
theory
SetMM
stx
1a7d4..
address
TMUBp..