Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cdiv (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cdif cc (csn cc0)) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) cmul) (cv x0)) (λ x2 . cc)))
as obj
-
as prop
416c1..
theory
SetMM
stx
a0443..
address
TMRqZ..