Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq csubrg (cmpt (λ x0 . crg) (λ x0 . crab (λ x1 . wa (wcel (co (cv x0) (cv x1) cress) crg) (wcel (cfv (cv x0) cur) (cv x1))) (λ x1 . cpw (cfv (cv x0) cbs))))
as obj
-
as prop
72f15..
theory
SetMM
stx
257fe..
address
TMUx1..