Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cidfu (cmpt (λ x0 . ccat) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . cop (cres cid (cv x1)) (cmpt (λ x2 . cxp (cv x1) (cv x1)) (λ x2 . cres cid (cfv (cv x2) (cfv (cv x0) chom)))))))
as obj
-
as prop
18b49..
theory
SetMM
stx
16f22..
address
TMFwm..