Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cmpq (cmpt2 (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cop (co (cfv (cv x0) c1st) (cfv (cv x1) c1st) cmi) (co (cfv (cv x0) c2nd) (cfv (cv x1) c2nd) cmi)))
as obj
-
as prop
ace13..
theory
SetMM
stx
338b7..
address
TMQyZ..