Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cmvr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cv x0) (λ x2 . cmpt (λ x3 . crab (λ x4 . wcel (cima (ccnv (cv x4)) cn) cfn) (λ x4 . co cn0 (cv x0) cmap)) (λ x3 . cif (wceq (cv x3) (cmpt (λ x4 . cv x0) (λ x4 . cif (wceq (cv x4) (cv x2)) c1 cc0))) (cfv (cv x1) cur) (cfv (cv x1) c0g)))))
as obj
-
as prop
cbc83..
theory
SetMM
stx
64ad5..
address
TMZzE..