Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cdgraa (cmpt (λ x0 . caa) (λ x0 . cinf (crab (λ x1 . wrex (λ x2 . wa (wceq (cfv (cv x2) cdgr) (cv x1)) (wceq (cfv (cv x0) (cv x2)) cc0)) (λ x2 . cdif (cfv cq cply) (csn c0p))) (λ x1 . cn)) cr clt))
as obj
-
as prop
ab244..
theory
SetMM
stx
c16e7..
address
TMMGA..