Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cltrr (copab (λ x0 x1 . wa (wa (wcel (cv x0) cr) (wcel (cv x1) cr)) (wex (λ x2 . wex (λ x3 . wa (wa (wceq (cv x0) (cop (cv x2) c0r)) (wceq (cv x1) (cop (cv x3) c0r))) (wbr (cv x2) (cv x3) cltr))))))
as obj
-
as prop
24703..
theory
SetMM
stx
96135..
address
TMamN..