Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cinito (cmpt (λ x0 . ccat) (λ x0 . crab (λ x1 . wral (λ x2 . weu (λ x3 . wcel (cv x3) (co (cv x1) (cv x2) (cfv (cv x0) chom)))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)))
as obj
-
as prop
acbb4..
theory
SetMM
stx
16f22..
address
TMLtP..