Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq chli (copab (λ x0 x1 . wa (wa (wf cn chil (cv x0)) (wcel (cv x1) chil)) (wral (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (co (cfv (cv x4) (cv x0)) (cv x1) cmv) cno) (cv x2) clt) (λ x4 . cfv (cv x3) cuz)) (λ x3 . cn)) (λ x2 . crp))))
as obj
-
as prop
e031d..
theory
SetMM
stx
5b3a9..
address
TMJED..