Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cai (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . crab (λ x2 . wfun (ccnv (cmpt (λ x3 . cfv (co (cv x2) (co (cv x0) (cv x1) cress) cmpl) cbs) (λ x3 . cfv (cres cid (cv x2)) (cfv (cv x3) (cfv (cv x1) (co (cv x2) (cv x0) ces))))))) (λ x2 . cpw (cfv (cv x0) cbs))))
as obj
-
as prop
f321c..
theory
SetMM
stx
4ed04..
address
TMbc5..