Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq csqrt (cmpt (λ x0 . cc) (λ x0 . crio (λ x1 . w3a (wceq (co (cv x1) c2 cexp) (cv x0)) (wbr cc0 (cfv (cv x1) cre) cle) (wnel (co ci (cv x1) cmul) crp)) (λ x1 . cc)))
as obj
-
as prop
4ff41..
theory
SetMM
stx
99b09..
address
TMNLP..