Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cxko (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cfv (cfv (crn (cmpt2 (λ x2 x3 . crab (λ x4 . wcel (co (cv x1) (cv x4) crest) ccmp) (λ x4 . cpw (cuni (cv x1)))) (λ x2 x3 . cv x0) (λ x2 x3 . crab (λ x4 . wss (cima (cv x4) (cv x2)) (cv x3)) (λ x4 . co (cv x1) (cv x0) ccn)))) cfi) ctg))
as obj
-
as prop
799ba..
theory
SetMM
stx
8519a..
address
TMGQ9..