Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq clf (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wceq (cfv (co (co (cv x1) (cv x2) csm) (cv x3) cva) (cv x0)) (co (co (cv x1) (cfv (cv x2) (cv x0)) cmul) (cfv (cv x3) (cv x0)) caddc)) (λ x3 . chil)) (λ x2 . chil)) (λ x1 . cc)) (λ x0 . co cc chil cmap))
as obj
-
as prop
353e3..
theory
SetMM
stx
99341..
address
TMXUZ..