Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cfwddif (cmpt (λ x0 . co cc cc cpm) (λ x0 . cmpt (λ x1 . crab (λ x2 . wcel (co (cv x2) c1 caddc) (cdm (cv x0))) (λ x2 . cdm (cv x0))) (λ x1 . co (cfv (co (cv x1) c1 caddc) (cv x0)) (cfv (cv x1) (cv x0)) cmin)))
as obj
-
as prop
bbf73..
theory
SetMM
stx
cb8e1..
address
TMEmg..