Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq ces1 (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . ccom (cmpt (λ x3 . co (cv x2) (co (cv x2) c1o cmap) cmap) (λ x3 . ccom (cv x3) (cmpt (λ x4 . cv x2) (λ x4 . cxp c1o (csn (cv x4)))))) (cfv (cv x1) (co c1o (cv x0) ces)))))
as obj
-
as prop
1b666..
theory
SetMM
stx
4ed04..
address
TMPMN..