Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cdenom (cmpt (λ x0 . cq) (λ x0 . cfv (crio (λ x1 . wa (wceq (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cgcd) c1) (wceq (cv x0) (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cdiv))) (λ x1 . cxp cz cn)) c2nd))
as obj
-
as prop
5b36b..
theory
SetMM
stx
0aa70..
address
TMSZ3..