Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cgzf (cab (λ x0 . w3a (w3a (wtr (cv x0)) (wbr (cv x0) cgze cprv) (wbr (cv x0) cgzp cprv)) (w3a (wbr (cv x0) cgzu cprv) (wbr (cv x0) cgzg cprv) (wbr (cv x0) cgzi cprv)) (wral (λ x1 . wbr (cv x0) (cfv (cv x1) cgzr) cprv) (λ x1 . cfv com cfmla))))
as obj
-
as prop
17a52..
theory
SetMM
stx
81cee..
address
TMcUF..