Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq clinco (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . crab (λ x2 . wrex (λ x3 . wa (wbr (cv x3) (cfv (cfv (cv x0) csca) c0g) cfsupp) (wceq (cv x2) (co (cv x3) (cv x1) (cfv (cv x0) clinc)))) (λ x3 . co (cfv (cfv (cv x0) csca) cbs) (cv x1) cmap)) (λ x2 . cfv (cv x0) cbs)))
as obj
-
as prop
04334..
theory
SetMM
stx
10cbd..
address
TMHoS..