Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cmpl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmps) (λ x2 . co (cv x2) (crab (λ x3 . wbr (cv x3) (cfv (cv x1) c0g) cfsupp) (λ x3 . cfv (cv x2) cbs)) cress)))
as obj
-
as prop
665d3..
theory
SetMM
stx
4ed04..
address
TMF8t..