Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cuvc (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cv x1) (λ x2 . cmpt (λ x3 . cv x1) (λ x3 . cif (wceq (cv x3) (cv x2)) (cfv (cv x0) cur) (cfv (cv x0) c0g)))))
as obj
-
as prop
e0003..
theory
SetMM
stx
9fb9c..
address
TMbCo..