Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cdv (cmpt2 (λ x0 x1 . cpw cc) (λ x0 x1 . co cc (cv x0) cpm) (λ x0 x1 . ciun (λ x2 . cfv (cdm (cv x1)) (cfv (co (cfv ccnfld ctopn) (cv x0) crest) cnt)) (λ x2 . cxp (csn (cv x2)) (co (cmpt (λ x3 . cdif (cdm (cv x1)) (csn (cv x2))) (λ x3 . co (co (cfv (cv x3) (cv x1)) (cfv (cv x2) (cv x1)) cmin) (co (cv x3) (cv x2) cmin) cdiv)) (cv x2) climc))))
as obj
-
as prop
3ed03..
theory
SetMM
stx
fc037..
address
TMaq5..