Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cordt (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cun (csn (cdm (cv x0))) (crn (cun (cmpt (λ x1 . cdm (cv x0)) (λ x1 . crab (λ x2 . wn (wbr (cv x2) (cv x1) (cv x0))) (λ x2 . cdm (cv x0)))) (cmpt (λ x1 . cdm (cv x0)) (λ x1 . crab (λ x2 . wn (wbr (cv x1) (cv x2) (cv x0))) (λ x2 . cdm (cv x0))))))) cfi) ctg))
as obj
-
as prop
00081..
theory
SetMM
stx
df09f..
address
TMUTN..