Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq csumge0 (cmpt (λ x0 . cvv) (λ x0 . cif (wcel cpnf (crn (cv x0))) cpnf (csup (crn (cmpt (λ x1 . cin (cpw (cdm (cv x0))) cfn) (λ x1 . csu (cv x1) (λ x2 . cfv (cv x2) (cv x0))))) cxr clt)))
as obj
-
as prop
43345..
theory
SetMM
stx
bfbce..
address
TMXog..