Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cpgp (copab (λ x0 x1 . wa (wa (wcel (cv x0) cprime) (wcel (cv x1) cgrp)) (wral (λ x2 . wrex (λ x3 . wceq (cfv (cv x2) (cfv (cv x1) cod)) (co (cv x0) (cv x3) cexp)) (λ x3 . cn0)) (λ x2 . cfv (cv x1) cbs))))
as obj
-
as prop
50ce8..
theory
SetMM
stx
ac091..
address
TMWB5..