Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq comn (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (cv x0)) (λ x0 x1 . cseq (ccom (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . cop (co (cfv (cfv (cv x2) c1st) ctopn) (cfv (cv x2) c2nd) comi) (cxp (co cc0 c1 cicc) (csn (cfv (cv x2) c2nd))))) c1st) (cop (cpr (cop (cfv cnx cbs) (cuni (cv x0))) (cop (cfv cnx cts) (cv x0))) (cv x1)) cc0))
as obj
-
as prop
71595..
theory
SetMM
stx
bc3a6..
address
TMa33..