Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq co1 (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wral (λ x3 . wbr (cfv (cfv (cv x3) (cv x0)) cabs) (cv x2) cle) (λ x3 . cin (cdm (cv x0)) (co (cv x1) cpnf cico))) (λ x2 . cr)) (λ x1 . cr)) (λ x0 . co cc cr cpm))
as obj
-
as prop
9f944..
theory
SetMM
stx
99b09..
address
TMTTV..