Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cfcls (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (crn cfil)) (λ x0 x1 . cif (wceq (cuni (cv x0)) (cuni (cv x1))) (ciin (λ x2 . cv x1) (λ x2 . cfv (cv x2) (cfv (cv x0) ccl))) c0))
as obj
-
as prop
9cda3..
theory
SetMM
stx
8519a..
address
TMPti..